--- a/IntEx.thy	Wed Nov 18 23:52:48 2009 +0100
+++ b/IntEx.thy	Thu Nov 19 14:17:10 2009 +0100
@@ -144,7 +144,17 @@
 
 print_quotients
 
-ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *}
+ML {* 
+  val test = lift_thm_my_int @{context} @{thm plus_sym_pre} 
+*}
+
+ML {* my_lift (prop_of test) @{thm plus_sym_pre} @{context} *}
+
+ML {*
+  ObjectLogic.atomize_term @{theory} (prop_of test)
+  |> Syntax.string_of_term @{context}
+  |> writeln
+*}
 
 lemma plus_assoc_pre:
   shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"