--- 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 =