--- a/IntEx.thy	Thu Nov 19 14:17:10 2009 +0100
+++ b/IntEx.thy	Fri Nov 20 13:03:01 2009 +0100
@@ -22,7 +22,6 @@
 
 ML {* print_qconstinfo @{context} *}
 
-
 term ZERO
 thm ZERO_def
 
@@ -143,19 +142,20 @@
 *}
 
 print_quotients
+ML {* quotdata_lookup @{context} "IntEx.my_int" *}
+ML {* quotdata_lookup @{context} "my_int" *}
 
 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
+  val aqtrm = HOLogic.dest_Trueprop (prop_of (atomize_thm test))
+  val artrm = HOLogic.dest_Trueprop (prop_of (atomize_thm @{thm plus_sym_pre})) 
 *}
 
+
 lemma plus_assoc_pre:
   shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
   apply (cases i)