diff --git a/src/HOL/Data_Structures/Queue_2Lists.thy b/src/HOL/Data_Structures/Queue_2Lists.thy
--- a/src/HOL/Data_Structures/Queue_2Lists.thy
+++ b/src/HOL/Data_Structures/Queue_2Lists.thy
@@ -1,86 +1,86 @@
 (* Author: Tobias Nipkow *)
 
 section \<open>Queue Implementation via 2 Lists\<close>
 
 theory Queue_2Lists
 imports Queue_Spec
 begin
 
 text \<open>Definitions:\<close>
 
 type_synonym 'a queue = "'a list \<times> 'a list"
 
 fun norm :: "'a queue \<Rightarrow> 'a queue" where
 "norm (os,is) = (if os = [] then (rev is, []) else (os,is))"
 
 fun enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
 "enq a (os,is) = norm(os, a # is)"
 
 fun deq :: "'a queue \<Rightarrow> 'a queue" where
 "deq (os,is) = (if os = [] then (os,is) else norm(tl os,is))"
 
-fun front :: "'a queue \<Rightarrow> 'a" where
-"front (a # os,is) = a"
+fun first :: "'a queue \<Rightarrow> 'a" where
+"first (a # os,is) = a"
 
 fun is_empty :: "'a queue \<Rightarrow> bool" where
 "is_empty (os,is) = (os = [])"
 
 fun list :: "'a queue \<Rightarrow> 'a list" where
 "list (os,is) = os @ rev is"
 
 fun invar :: "'a queue \<Rightarrow> bool" where
 "invar (os,is) = (os = [] \<longrightarrow> is = [])"
 
 
 text \<open>Implementation correctness:\<close>
 
 interpretation Queue
-where empty = "([],[])" and enq = enq and deq = deq and front = front
+where empty = "([],[])" and enq = enq and deq = deq and first = first
 and is_empty = is_empty and list = list and invar = invar
 proof (standard, goal_cases)
   case 1 show ?case by (simp)
 next
   case (2 q) thus ?case by(cases q) (simp)
 next
   case (3 q) thus ?case by(cases q) (simp)
 next
   case (4 q) thus ?case by(cases q) (auto simp: neq_Nil_conv)
 next
   case (5 q) thus ?case by(cases q) (auto)
 next
   case 6 show ?case by(simp)
 next
   case (7 q) thus ?case by(cases q) (simp)
 next
   case (8 q) thus ?case by(cases q) (simp)
 qed
 
 text \<open>Running times:\<close>
 
 fun t_norm :: "'a queue \<Rightarrow> nat" where
 "t_norm (os,is) = (if os = [] then length is else 0) + 1"
 
 fun t_enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> nat" where
 "t_enq a (os,is) = t_norm(os, a # is)"
 
 fun t_deq :: "'a queue \<Rightarrow> nat" where
 "t_deq (os,is) = (if os = [] then 0 else t_norm(tl os,is)) + 1"
 
-fun t_front :: "'a queue \<Rightarrow> nat" where
-"t_front (a # os,is) = 1"
+fun t_first :: "'a queue \<Rightarrow> nat" where
+"t_first (a # os,is) = 1"
 
 fun t_is_empty :: "'a queue \<Rightarrow> nat" where
 "t_is_empty (os,is) = 1"
 
 text \<open>Amortized running times:\<close>
 
 fun \<Phi> :: "'a queue \<Rightarrow> nat" where
 "\<Phi>(os,is) = length is"
 
 lemma a_enq: "t_enq a (os,is) + \<Phi>(enq a (os,is)) - \<Phi>(os,is) \<le> 2"
 by(auto)
 
 lemma a_deq: "t_deq (os,is) + \<Phi>(deq (os,is)) - \<Phi>(os,is) \<le> 2"
 by(auto)
 
 end
diff --git a/src/HOL/Data_Structures/Queue_Spec.thy b/src/HOL/Data_Structures/Queue_Spec.thy
--- a/src/HOL/Data_Structures/Queue_Spec.thy
+++ b/src/HOL/Data_Structures/Queue_Spec.thy
@@ -1,28 +1,28 @@
 (* Author: Tobias Nipkow *)
 
 section \<open>Queue Specification\<close>
 
 theory Queue_Spec
 imports Main
 begin
 
 text \<open>The basic queue interface with \<open>list\<close>-based specification:\<close>
 
 locale Queue =
 fixes empty :: "'q"
 fixes enq :: "'a \<Rightarrow> 'q \<Rightarrow> 'q"
-fixes front :: "'q \<Rightarrow> 'a"
+fixes first :: "'q \<Rightarrow> 'a"
 fixes deq :: "'q \<Rightarrow> 'q"
 fixes is_empty :: "'q \<Rightarrow> bool"
 fixes list :: "'q \<Rightarrow> 'a list"
 fixes invar :: "'q \<Rightarrow> bool"
 assumes list_empty:    "list empty = []"
 assumes list_enq:      "invar q \<Longrightarrow> list(enq x q) = list q @ [x]"
 assumes list_deq:      "invar q \<Longrightarrow> list(deq q) = tl(list q)"
-assumes list_front:    "invar q \<Longrightarrow> \<not> list q = [] \<Longrightarrow> front q = hd(list q)"
+assumes list_first:    "invar q \<Longrightarrow> \<not> list q = [] \<Longrightarrow> first q = hd(list q)"
 assumes list_is_empty: "invar q \<Longrightarrow> is_empty q = (list q = [])"
 assumes invar_empty:   "invar empty"
 assumes invar_enq:     "invar q \<Longrightarrow> invar(enq x q)"
 assumes invar_deq:     "invar q \<Longrightarrow> invar(deq q)"
 
 end