diff -r df053507edba -r 37285ec4387d Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/Examples/LamEx.thy	Sun Dec 20 00:53:35 2009 +0100
@@ -56,17 +56,17 @@
 
 print_quotients
 
-quotient_def
+quotient_definition
    "Var :: name \<Rightarrow> lam"
 as
   "rVar"
 
-quotient_def
+quotient_definition
    "App :: lam \<Rightarrow> lam \<Rightarrow> lam"
 as
   "rApp"
 
-quotient_def
+quotient_definition
    "Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
 as
   "rLam"
@@ -75,7 +75,7 @@
 thm App_def
 thm Lam_def
 
-quotient_def
+quotient_definition
    "fv :: lam \<Rightarrow> name set"
 as
   "rfv"
@@ -88,7 +88,7 @@
   perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"   (unchecked)
 begin
 
-quotient_def
+quotient_definition
    "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"
 as
   "perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam"