diff -r ca37f4b6457c -r 8dfae5d97387 Quot/Examples/LFex.thy
--- a/Quot/Examples/LFex.thy	Tue Dec 08 11:17:56 2009 +0100
+++ b/Quot/Examples/LFex.thy	Tue Dec 08 11:20:01 2009 +0100
@@ -218,12 +218,6 @@
 thm akind_aty_atrm.induct
 thm kind_ty_trm.induct
 
-ML {*
-  val quot = @{thms Quotient_KIND Quotient_TY Quotient_TRM}
-  val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) @{thms alpha_equivps}
-  val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quot
-  val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quot
-*}
 
 lemma 
   assumes a0:
@@ -261,7 +255,7 @@
 apply - 
 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} 1 *})
 apply(fold perm_kind_def perm_ty_def perm_trm_def)
 apply(tactic {* clean_tac @{context} 1 *})
 (*