diff -r 2d9de77d5687 -r 0dd10a900cae Quot/Examples/LFex.thy
--- a/Quot/Examples/LFex.thy	Wed Dec 09 06:21:09 2009 +0100
+++ b/Quot/Examples/LFex.thy	Wed Dec 09 15:57:47 2009 +0100
@@ -82,51 +82,51 @@
 
 print_quotients
 
-quotient_def 
-  TYP :: "KIND"
+quotient_def
+  TYP :: "TYP :: KIND"
 where
-  "TYP \<equiv> Type"
+  "Type"
 
-quotient_def 
-  KPI :: "TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
+quotient_def
+  KPI :: "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
 where
-  "KPI \<equiv> KPi"
+  "KPi"
 
-quotient_def 
-  TCONST :: "ident \<Rightarrow> TY"
+quotient_def
+  TCONST :: "TCONST :: ident \<Rightarrow> TY"
 where
-  "TCONST \<equiv> TConst"
+  "TConst"
 
-quotient_def 
-  TAPP :: "TY \<Rightarrow> TRM \<Rightarrow> TY"
+quotient_def
+  TAPP :: "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
 where
-  "TAPP \<equiv> TApp"
+  "TApp"
 
-quotient_def 
-  TPI :: "TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
+quotient_def
+  TPI :: "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
 where
-  "TPI \<equiv> TPi"
+  "TPi"
 
 (* FIXME: does not work with CONST *)
-quotient_def 
-  CONS :: "ident \<Rightarrow> TRM"
+quotient_def
+  CONS :: "CONS :: ident \<Rightarrow> TRM"
 where
-  "CONS \<equiv> Const"
+  "Const"
 
-quotient_def 
-  VAR :: "name \<Rightarrow> TRM"
+quotient_def
+  VAR :: "VAR :: name \<Rightarrow> TRM"
 where
-  "VAR \<equiv> Var"
+  "Var"
 
-quotient_def 
-  APP :: "TRM \<Rightarrow> TRM \<Rightarrow> TRM"
+quotient_def
+  APP :: "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
 where
-  "APP \<equiv> App"
+  "App"
 
-quotient_def 
-  LAM :: "TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
+quotient_def
+  LAM :: "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
 where
-  "LAM \<equiv> Lam"
+  "Lam"
 
 thm TYP_def
 thm KPI_def
@@ -139,20 +139,20 @@
 thm LAM_def
 
 (* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
-quotient_def 
-  FV_kind :: "KIND \<Rightarrow> name set"
+quotient_def
+  FV_kind :: "FV_kind :: KIND \<Rightarrow> name set"
 where
-  "FV_kind \<equiv> fv_kind"
+  "fv_kind"
 
-quotient_def 
-  FV_ty :: "TY \<Rightarrow> name set"
+quotient_def
+  FV_ty :: "FV_ty :: TY \<Rightarrow> name set"
 where
-  "FV_ty \<equiv> fv_ty"
+  "fv_ty"
 
-quotient_def 
-  FV_trm :: "TRM \<Rightarrow> name set"
+quotient_def
+  FV_trm :: "FV_trm :: TRM \<Rightarrow> name set"
 where
-  "FV_trm \<equiv> fv_trm"
+  "fv_trm"
 
 thm FV_kind_def
 thm FV_ty_def
@@ -165,20 +165,20 @@
     perm_trm  \<equiv> "perm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"     (unchecked) 
 begin
 
-quotient_def 
-  perm_kind :: "'x prm \<Rightarrow> KIND \<Rightarrow> KIND"
+quotient_def
+  perm_kind :: "perm_kind :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND"
 where
-  "perm_kind \<equiv> (perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)"
+  "(perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)"
 
-quotient_def 
-  perm_ty :: "'x prm \<Rightarrow> TY \<Rightarrow> TY"
+quotient_def
+  perm_ty :: "perm_ty :: 'x prm \<Rightarrow> TY \<Rightarrow> TY"
 where
-  "perm_ty \<equiv> (perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)"
+  "(perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)"
 
-quotient_def 
-  perm_trm :: "'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
+quotient_def
+  perm_trm :: "perm_trm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
 where
-  "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
+  "(perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
 
 end
 
@@ -253,9 +253,6 @@
          ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"
 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
 apply(lifting akind_aty_atrm.induct)
-(* FIXME: with overloaded definitions *)
-apply(fold perm_kind_def perm_ty_def perm_trm_def)
-apply(cleaning)
 (*
 Profiling:
 ML_prf {* fun ith i =  (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *}