diff -r 38aa6b67a80b -r 2bee5ca44ef5 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Mon Dec 07 18:49:14 2009 +0100
+++ b/Quot/Examples/FSet.thy	Mon Dec 07 21:53:50 2009 +0100
@@ -303,7 +303,7 @@
 lemma "IN x EMPTY = False"
 apply(tactic {* procedure_tac @{context} @{thm m1} 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(tactic {* clean_tac @{context} 1*})
 done
 
@@ -331,8 +331,6 @@
 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 done
 
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
-
 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
 done
@@ -348,7 +346,7 @@
 apply(tactic {* regularize_tac @{context} 1 *})
 defer
 apply(tactic {* clean_tac @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1*})+
+apply(tactic {* inj_repabs_tac @{context} 1*})+
 done
 
 lemma list_induct_part:
@@ -390,10 +388,6 @@
 where
   "INSERT2 \<equiv> op #"
 
-ML {* val quot = @{thms Quotient_fset Quotient_fset2} *}
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t  *}
-
 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
 done
@@ -425,9 +419,6 @@
   apply (auto)
   sorry
 
-ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t *}
-
 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
 done