--- a/QuotMain.thy	Wed Nov 18 23:52:48 2009 +0100
+++ b/QuotMain.thy	Thu Nov 19 14:17:10 2009 +0100
@@ -1074,7 +1074,8 @@
 
 
 ML {*
-fun lift_thm lthy qty qty_name rsp_thms defs rthm = 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;
@@ -1133,7 +1134,6 @@
 end
 *}
 
-
 ML {*
 fun lift_thm_note qty qty_name rsp_thms defs thm name lthy =
   let
@@ -1144,7 +1144,20 @@
   end
 *}
 
+ML {*
+fun my_lift qtrm rthm lthy =
+let
+  val thy = ProofContext.theory_of lthy
 
+  val a_rthm = atomize_thm rthm
+  val a_qtrm = ObjectLogic.atomize_term thy qtrm
+
+  val _ = Syntax.string_of_term lthy (prop_of a_rthm) |> writeln
+  val _ = Syntax.string_of_term lthy a_qtrm |> writeln
+in
+  (a_rthm, a_qtrm)
+end
+*}
 
 end