--- a/FSet.thy	Mon Nov 30 15:40:22 2009 +0100
+++ b/FSet.thy	Tue Dec 01 12:16:45 2009 +0100
@@ -308,12 +308,7 @@
 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
 apply(tactic {* regularize_tac @{context}  [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-ML_prf {* 
-  val rtrm = @{term "\<forall>x. IN x EMPTY = False"}
-  val qtrm = @{term "\<forall>x. x memb [] = False"}
-  val aps = find_aps rtrm qtrm 
-*}
-apply(tactic {* clean_tac @{context} [quot] defs aps 1*})
+apply(tactic {* clean_tac @{context} [quot] defs 1*})
 done
 
 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
@@ -358,7 +353,7 @@
 apply(tactic {* procedure_tac @{context} @{thm list.induct} 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] defs 1 *})
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
@@ -456,7 +451,7 @@
 apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})
 apply (tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 prefer 2
-apply (tactic {* clean_tac @{context} [quot] defs [(@{typ "('a list \<Rightarrow> 'c list \<Rightarrow> bool)"},@{typ "('a list \<Rightarrow> 'c fset \<Rightarrow> bool)"})] 1 *})
+apply (tactic {* clean_tac @{context} [quot] defs 1 *})
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 apply (rule FUN_QUOTIENT)
 apply (rule FUN_QUOTIENT)

--- a/IntEx.thy	Mon Nov 30 15:40:22 2009 +0100
+++ b/IntEx.thy	Tue Dec 01 12:16:45 2009 +0100
@@ -150,9 +150,7 @@
 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 prefer 2
-ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
-ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
-apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
+apply(tactic {* clean_tac @{context} [quot] defs 1 *})
 apply(simp add: id_def)
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
@@ -194,9 +192,7 @@
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(simp)
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
-ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
-apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
+apply(tactic {* clean_tac @{context} [quot] defs 1 *})
 done
 
 lemma ho_tst: "foldl my_plus x [] = x"
@@ -217,10 +213,8 @@
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(simp add: map_prs)
-ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
-ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm ho_tst})) (term_of qtm) *}
 apply(simp only: map_prs)
-apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
+apply(tactic {* clean_tac @{context} [quot] defs 1 *})
 sorry
 
 (*
@@ -233,9 +227,7 @@
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(simp)
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) 
-ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
-ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
-apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
+apply(tactic {* clean_tac @{context} [quot] defs 1 *})
 done
 
 

--- a/LFex.thy	Mon Nov 30 15:40:22 2009 +0100
+++ b/LFex.thy	Tue Dec 01 12:16:45 2009 +0100
@@ -265,9 +265,6 @@
          ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"
 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
 apply - 
-apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
-ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
-ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm akind_aty_atrm.induct})) (term_of qtm) *}
 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
@@ -461,7 +458,7 @@
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2  1*})
-apply(tactic {* clean_tac @{context} quot defs aps 1 *})
+apply(tactic {* clean_tac @{context} quot defs 1 *})
 done
 
 (* Does not work:
@@ -488,14 +485,8 @@
   \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2);
   \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk>
   \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm"
-
-apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
-ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
-ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm kind_ty_trm.induct})) (term_of qtm) *}
 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *})
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
-prefer 2
-apply(tactic {* clean_tac @{context} quot defs aps 1 *})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *})
@@ -587,6 +578,7 @@
 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
+apply(tactic {* clean_tac @{context} quot defs 1 *})
 done
 
 print_quotients

--- a/QuotMain.thy	Mon Nov 30 15:40:22 2009 +0100
+++ b/QuotMain.thy	Tue Dec 01 12:16:45 2009 +0100
@@ -791,7 +791,7 @@
 lemma FUN_REL_I:
   assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
   shows "(R1 ===> R2) f g"
-using a by (simp add: FUN_REL.simps)
+using a by simp
 
 ML {*
 val lambda_res_tac =
@@ -949,47 +949,6 @@
 
 section {* Cleaning of the theorem *}
 
-ML {*
-fun applic_prs lthy absrep (rty, qty) =
-  let
-    fun mk_rep (T, T') tm = (Quotient_Def.get_fun repF lthy (T, T')) $ tm;
-    fun mk_abs (T, T') tm = (Quotient_Def.get_fun absF lthy (T, T')) $ tm;
-    val (raty, rgty) = Term.strip_type rty;
-    val (qaty, qgty) = Term.strip_type qty;
-    val vs = map (fn _ => "x") qaty;
-    val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
-    val f = Free (fname, qaty ---> qgty);
-    val args = map Free (vfs ~~ qaty);
-    val rhs = list_comb(f, args);
-    val largs = map2 mk_rep (raty ~~ qaty) args;
-    val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs));
-    val llhs = Syntax.check_term lthy lhs;
-    val eq = Logic.mk_equals (llhs, rhs);
-    val ceq = cterm_of (ProofContext.theory_of lthy') eq;
-    val sctxt = HOL_ss addsimps (@{thms fun_map.simps id_simps} @ absrep);
-    val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
-    val t_id = MetaSimplifier.rewrite_rule @{thms id_simps} t;
-  in
-    singleton (ProofContext.export lthy' lthy) t_id
-  end
-*}
-
-ML {*
-fun find_aps_all rtm qtm =
-  case (rtm, qtm) of
-    (Abs(_, T1, s1), Abs(_, T2, s2)) =>
-      find_aps_all (subst_bound ((Free ("x", T1)), s1)) (subst_bound ((Free ("x", T2)), s2))
-  | (((f1 as (Free (_, T1))) $ a1), ((f2 as (Free (_, T2))) $ a2)) =>
-      let
-        val sub = (find_aps_all f1 f2) @ (find_aps_all a1 a2)
-      in
-        if T1 = T2 then sub else (T1, T2) :: sub
-      end
-  | ((f1 $ a1), (f2 $ a2)) => (find_aps_all f1 f2) @ (find_aps_all a1 a2)
-  | _ => [];
-
-fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm)
-*}
 
 (* TODO: This is slow *)
 ML {*
@@ -1086,7 +1045,7 @@
  The rest are a simp_tac and are fast.
 *)
 ML {*
-fun clean_tac lthy quot defs aps =
+fun clean_tac lthy quot defs =
   let
     val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot
     val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep;
@@ -1210,7 +1169,6 @@
     let
       val rthm' = atomize_thm rthm
       val rule = procedure_inst context (prop_of rthm') (term_of concl)
-      val aps = find_aps (prop_of rthm') (term_of concl)
       val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv
       val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv
     in
@@ -1219,7 +1177,7 @@
         RANGE [rtac rthm',
                regularize_tac lthy rel_eqv,
                all_inj_repabs_tac lthy rty quot rel_refl trans2,
-               clean_tac lthy quot defs aps]]
+               clean_tac lthy quot defs]]
     end) lthy
 *}
 

--- a/UnusedQuotMain.thy	Mon Nov 30 15:40:22 2009 +0100
+++ b/UnusedQuotMain.thy	Tue Dec 01 12:16:45 2009 +0100
@@ -1,3 +1,8 @@
+(* Code for getting the goal *)
+apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
+ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
+
+
 ML {*
 fun repeat_eqsubst_thm ctxt thms thm =
   repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)
@@ -487,6 +492,49 @@
 ML {* atomize_goal @{theory} @{term "x = xa ? a # x = a # xa"} *}
 
 
+ML {*
+fun applic_prs lthy absrep (rty, qty) =
+  let
+    fun mk_rep (T, T') tm = (Quotient_Def.get_fun repF lthy (T, T')) $ tm;
+    fun mk_abs (T, T') tm = (Quotient_Def.get_fun absF lthy (T, T')) $ tm;
+    val (raty, rgty) = Term.strip_type rty;
+    val (qaty, qgty) = Term.strip_type qty;
+    val vs = map (fn _ => "x") qaty;
+    val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
+    val f = Free (fname, qaty ---> qgty);
+    val args = map Free (vfs ~~ qaty);
+    val rhs = list_comb(f, args);
+    val largs = map2 mk_rep (raty ~~ qaty) args;
+    val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs));
+    val llhs = Syntax.check_term lthy lhs;
+    val eq = Logic.mk_equals (llhs, rhs);
+    val ceq = cterm_of (ProofContext.theory_of lthy') eq;
+    val sctxt = HOL_ss addsimps (@{thms fun_map.simps id_simps} @ absrep);
+    val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
+    val t_id = MetaSimplifier.rewrite_rule @{thms id_simps} t;
+  in
+    singleton (ProofContext.export lthy' lthy) t_id
+  end
+*}
+
+ML {*
+fun find_aps_all rtm qtm =
+  case (rtm, qtm) of
+    (Abs(_, T1, s1), Abs(_, T2, s2)) =>
+      find_aps_all (subst_bound ((Free ("x", T1)), s1)) (subst_bound ((Free ("x", T2)), s2))
+  | (((f1 as (Free (_, T1))) $ a1), ((f2 as (Free (_, T2))) $ a2)) =>
+      let
+        val sub = (find_aps_all f1 f2) @ (find_aps_all a1 a2)
+      in
+        if T1 = T2 then sub else (T1, T2) :: sub
+      end
+  | ((f1 $ a1), (f2 $ a2)) => (find_aps_all f1 f2) @ (find_aps_all a1 a2)
+  | _ => [];
+
+fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm)
+*}
+
+
 
 ML {*
 fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal =