--- a/QuotMain.thy	Tue Nov 03 16:17:19 2009 +0100
+++ b/QuotMain.thy	Tue Nov 03 17:30:27 2009 +0100
@@ -960,6 +960,37 @@
   end
 *}
 
+ML {*
+fun applic_prs lthy rty qty absrep ty =
+ let
+  fun absty ty =
+    old_exchange_ty rty qty ty
+  fun mk_rep tm =
+    let
+      val ty = old_exchange_ty rty qty (fastype_of tm)
+    in fst (old_get_fun repF rty qty lthy ty) $ tm end;
+  fun mk_abs tm =
+      let
+        val ty = old_exchange_ty rty qty (fastype_of tm) in
+      fst (old_get_fun absF rty qty lthy ty) $ tm end;
+  val (l, ltl) = Term.strip_type ty;
+  val nl = map absty l;
+  val vs = map (fn _ => "x") l;
+  val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
+  val args = map Free (vfs ~~ nl);
+  val lhs = list_comb((Free (fname, nl ---> ltl)), args);
+  val rargs = map mk_rep args;
+  val f = Free (fname, nl ---> ltl);
+  val rhs = mk_abs (list_comb((mk_rep f), rargs));
+  val eq = Logic.mk_equals (rhs, lhs);
+  val ceq = cterm_of (ProofContext.theory_of lthy') eq;
+  val sctxt = (Simplifier.context lthy' HOL_ss) addsimps (absrep :: @{thms fun_map.simps});
+  val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
+  val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t;
+ in
+  singleton (ProofContext.export lthy' lthy) t_id
+ end
+*}
 
 ML {*
 fun lookup_quot_data lthy qty =
@@ -981,9 +1012,10 @@
     val thy = ProofContext.theory_of lthy;
     val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")
     val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")
+    val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10")
     val quot = PureThy.get_thm thy ("QUOTIENT_" ^ qty_name)
   in
-    (trans2, reps_same, quot)
+    (trans2, reps_same, absrep, quot)
   end
 *}
 
@@ -1000,7 +1032,7 @@
 ML {*
 fun lift_thm lthy qty qty_name rsp_thms defs t = let
   val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;
-  val (trans2, reps_same, quot) = lookup_quot_thms lthy qty_name;
+  val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;
   val consts = lookup_quot_consts defs;
   val t_a = atomize_thm t;
   val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;
@@ -1011,7 +1043,7 @@
   val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t
   val abs = findabs rty (prop_of t_a);
   val aps = findaps rty (prop_of t_a);
-  val app_prs_thms = map (make_simp_prs_thm lthy quot @{thm APP_PRS}) aps;
+  val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;
   val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;
   val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;
   val defs_sym = add_lower_defs lthy defs;