diff -r 0fd4abb5fade -r f51c6069cd17 Quot/Examples/LFex.thy
--- a/Quot/Examples/LFex.thy	Fri Dec 11 08:28:41 2009 +0100
+++ b/Quot/Examples/LFex.thy	Fri Dec 11 11:08:58 2009 +0100
@@ -81,49 +81,49 @@
   by (auto intro: alpha_equivps)
 
 quotient_def
-  TYP :: "TYP :: KIND"
-where
+   "TYP :: KIND"
+as
   "Type"
 
 quotient_def
-  KPI :: "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
-where
+   "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
+as
   "KPi"
 
 quotient_def
-  TCONST :: "TCONST :: ident \<Rightarrow> TY"
-where
+   "TCONST :: ident \<Rightarrow> TY"
+as
   "TConst"
 
 quotient_def
-  TAPP :: "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
-where
+   "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
+as
   "TApp"
 
 quotient_def
-  TPI :: "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
-where
+   "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
+as
   "TPi"
 
 (* FIXME: does not work with CONST *)
 quotient_def
-  CONS :: "CONS :: ident \<Rightarrow> TRM"
-where
+   "CONS :: ident \<Rightarrow> TRM"
+as
   "Const"
 
 quotient_def
-  VAR :: "VAR :: name \<Rightarrow> TRM"
-where
+   "VAR :: name \<Rightarrow> TRM"
+as
   "Var"
 
 quotient_def
-  APP :: "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
-where
+   "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
+as
   "App"
 
 quotient_def
-  LAM :: "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
-where
+   "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
+as
   "Lam"
 
 thm TYP_def
@@ -138,18 +138,18 @@
 
 (* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
 quotient_def
-  FV_kind :: "FV_kind :: KIND \<Rightarrow> name set"
-where
+   "FV_kind :: KIND \<Rightarrow> name set"
+as
   "fv_kind"
 
 quotient_def
-  FV_ty :: "FV_ty :: TY \<Rightarrow> name set"
-where
+   "FV_ty :: TY \<Rightarrow> name set"
+as
   "fv_ty"
 
 quotient_def
-  FV_trm :: "FV_trm :: TRM \<Rightarrow> name set"
-where
+   "FV_trm :: TRM \<Rightarrow> name set"
+as
   "fv_trm"
 
 thm FV_kind_def
@@ -164,18 +164,18 @@
 begin
 
 quotient_def
-  perm_kind :: "perm_kind :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND"
-where
+   "perm_kind :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND"
+as
   "(perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)"
 
 quotient_def
-  perm_ty :: "perm_ty :: 'x prm \<Rightarrow> TY \<Rightarrow> TY"
-where
+   "perm_ty :: 'x prm \<Rightarrow> TY \<Rightarrow> TY"
+as
   "(perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)"
 
 quotient_def
-  perm_trm :: "perm_trm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
-where
+   "perm_trm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
+as
   "(perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
 
 end