--- a/Quot/Examples/LarryDatatype.thy	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/Examples/LarryDatatype.thy	Sun Dec 20 00:53:35 2009 +0100
@@ -126,22 +126,22 @@
 
 text{*The abstract message constructors*}
 
-quotient_def
+quotient_definition
   "Nonce :: nat \<Rightarrow> msg"
 as
   "NONCE"
 
-quotient_def
+quotient_definition
   "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
 as
   "MPAIR"
 
-quotient_def
+quotient_definition
   "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
 as
   "CRYPT"
 
-quotient_def
+quotient_definition
   "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
 as
   "DECRYPT"
@@ -163,7 +163,7 @@
 
 subsection{*The Abstract Function to Return the Set of Nonces*}
 
-quotient_def
+quotient_definition
    "nonces:: msg \<Rightarrow> nat set"
 as
   "freenonces"
@@ -199,7 +199,7 @@
 
 subsection{*The Abstract Function to Return the Left Part*}
 
-quotient_def
+quotient_definition
   "left:: msg \<Rightarrow> msg"
 as
   "freeleft"
@@ -226,7 +226,7 @@
 
 subsection{*The Abstract Function to Return the Right Part*}
 
-quotient_def
+quotient_definition
   "right:: msg \<Rightarrow> msg"
 as
   "freeright"
@@ -360,7 +360,7 @@
 text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
 need this function in order to prove discrimination theorems.*}
 
-quotient_def
+quotient_definition
   "discrim:: msg \<Rightarrow> int"
 as
   "freediscrim"