--- a/Quot/Examples/IntEx.thy	Mon Dec 07 18:49:14 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Mon Dec 07 21:53:50 2009 +0100
@@ -136,15 +136,6 @@
   shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
 by (simp)
 
-ML {* val qty = @{typ "my_int"} *}
-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 {* fun lift_tac_intex lthy t = lift_tac lthy t *}
-
-ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
-ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *}
-
 lemma test1: "my_plus a b = my_plus a b"
 apply(rule refl)
 done
@@ -152,7 +143,7 @@
 lemma "PLUS a b = PLUS a b"
 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *}) 
 done
 
@@ -162,13 +153,15 @@
 apply(rule refl)
 done
 
+
+
 lemma "PLUS a = PLUS a"
 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *})
 apply(rule impI)
 apply(rule ballI)
 apply(rule apply_rsp[OF Quotient_my_int plus_rsp])
 apply(simp only: in_respects)
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
 
@@ -180,7 +173,7 @@
 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
 apply(rule impI)
 apply(rule plus_rsp)
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
 
@@ -188,7 +181,7 @@
 lemma "PLUS a b = PLUS b a"
 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
 
@@ -203,7 +196,7 @@
 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
 
@@ -214,7 +207,7 @@
 lemma "foldl PLUS x [] = x"
 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
 done
@@ -225,7 +218,7 @@
 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"
 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int])
 done
@@ -236,7 +229,7 @@
 lemma "foldl f (x::my_int) ([]::my_int list) = x"
 apply(tactic {* procedure_tac @{context} @{thm ho_tst3} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 (* TODO: does not work when this is added *)
 (* apply(tactic {* lambda_prs_tac @{context} 1 *})*)
 apply(tactic {* clean_tac @{context} 1 *})
@@ -249,7 +242,7 @@
 lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 apply(simp add: pair_prs)
 done
@@ -311,7 +304,7 @@
 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *})
 defer
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac  @{context} 1 *})
 apply(subst babs_rsp)
 apply(tactic {* clean_tac  @{context} 1 *})
@@ -329,7 +322,7 @@
 lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst3b} 1 *})
 defer
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac  @{context} 1 *})
 apply(subst babs_rsp)
 apply(tactic {* clean_tac  @{context} 1 *})