--- a/QuotMain.thy	Thu Nov 12 13:57:20 2009 +0100
+++ b/QuotMain.thy	Fri Nov 13 16:44:36 2009 +0100
@@ -250,7 +250,12 @@
         | _ => HOLogic.eq_const ty)
 *}
 
-(* ML {* cterm_of @{theory} (tyRel @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"}) @{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> bool)"} @{context}) *} *)
+(* 
+ML {* cterm_of @{theory} 
+  (tyRel @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"}) 
+         @{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> bool)"} @{context}) 
+*} 
+*)
 
 definition
   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
@@ -1069,29 +1074,60 @@
 
 
 ML {*
-fun lift_thm lthy qty qty_name rsp_thms defs t = let
+fun lift_thm lthy qty qty_name rsp_thms defs rthm = let
+  val _ = tracing ("raw theorem:\n" ^ Syntax.string_of_term lthy (prop_of rthm))
+
   val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;
   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_a = atomize_thm rthm;
+
+  val _ = tracing ("raw atomized theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_a))
+
   val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;
+
+  val _ = tracing ("regularised theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_r))
+
   val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
+
+  val _ = tracing ("rep/abs injected theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_t))
+
   val (alls, exs) = findallex lthy rty qty (prop_of t_a);
   val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls
   val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs
   val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t
+
+  val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_a))
+
   val abs = findabs rty (prop_of t_a);
   val aps = findaps rty (prop_of t_a);
   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 _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_l))
+
   val defs_sym = flat (map (add_lower_defs lthy) defs);
   val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;
   val t_id = simp_ids lthy t_l;
+
+  val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_id))
+
   val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;
+
+  val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d0))
+
   val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;
+
+  val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d))
+
   val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
+
+  val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_r))
+
   val t_rv = ObjectLogic.rulify t_r
+
+  val _ = tracing ("lifted theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_rv))
 in
   Thm.varifyT t_rv
 end