diff -r ce1f8a284920 -r 42082fc00903 QuotMain.thy
--- 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
 *}