diff -r f122816d7729 -r 184d74813679 IntEx.thy
--- a/IntEx.thy	Thu Dec 03 12:33:05 2009 +0100
+++ b/IntEx.thy	Thu Dec 03 13:45:52 2009 +0100
@@ -135,12 +135,10 @@
 ML {* val qty = @{typ "my_int"} *}
 ML {* val ty_name = "my_int" *}
 ML {* val rsp_thms = @{thms ho_plus_rsp} *}
-ML {* val defs = @{thms PLUS_def} *}
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
-ML {* val consts = lookup_quot_consts defs *}
 
-ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] [quot] defs *}
+ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] [quot] *}
 
 ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [quot] [rel_refl] [trans2] *}
 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [quot] [rel_refl] [trans2] *}
@@ -150,7 +148,7 @@
 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 prefer 2
-apply(tactic {* clean_tac @{context} [quot] defs 1 *})
+apply(tactic {* clean_tac @{context} [quot] 1 *})
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
@@ -188,7 +186,7 @@
 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* clean_tac @{context} [quot] defs 1 *})
+apply(tactic {* clean_tac @{context} [quot] 1 *})
 done
 
 lemma ho_tst: "foldl my_plus x [] = x"
@@ -285,7 +283,7 @@
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
 apply(simp only: nil_prs)
-apply(tactic {* clean_tac @{context} [quot] defs 1 *})
+apply(tactic {* clean_tac @{context} [quot] 1 *})
 done
 
 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
@@ -297,6 +295,6 @@
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
 apply(simp only: cons_prs[OF QUOTIENT_my_int])
-apply(tactic {* clean_tac @{context} [quot] defs 1 *})
+apply(tactic {* clean_tac @{context} [quot] 1 *})
 done