--- 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)"

--- a/Prove.thy	Wed Nov 18 23:52:48 2009 +0100
+++ b/Prove.thy	Thu Nov 19 14:17:10 2009 +0100
@@ -9,7 +9,7 @@
 ML {*
 let
   fun after_qed thm_name thms lthy =
-       LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd
+       Local_Theory.note (thm_name, (flat thms)) lthy |> snd
     
   fun setup_proof (name_spec, (txt, pos)) lthy =
   let

--- 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
 

--- a/quotient.ML	Wed Nov 18 23:52:48 2009 +0100
+++ b/quotient.ML	Thu Nov 19 14:17:10 2009 +0100
@@ -13,14 +13,14 @@
 fun define (name, mx, rhs) lthy =
 let
   val ((rhs, (_ , thm)), lthy') =
-     LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthy
+     Local_Theory.define "" ((name, mx), (Attrib.empty_binding, rhs)) lthy
 in
   ((rhs, thm), lthy')
 end
 
 fun note (name, thm) lthy =
 let
-  val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy
+  val ((_,[thm']), lthy') = Local_Theory.note ((name, []), [thm]) lthy
 in
   (thm', lthy')
 end
@@ -59,7 +59,7 @@
              rtac @{thm refl}]
   val tfrees = map fst (Term.add_tfreesT rty [])
 in
-  LocalTheory.theory_result
+  Local_Theory.theory_result
     (Typedef.add_typedef false NONE
        (qty_name, tfrees, mx)
          (typedef_term rel rty lthy)
@@ -172,7 +172,7 @@
   lthy5
   |> note (quot_thm_name, quot_thm)
   ||>> note (quotient_thm_name, quotient_thm)
-  ||> LocalTheory.theory (fn thy =>
+  ||> Local_Theory.theory (fn thy =>
       let
         val global_eqns = map exp_term [eqn2i, eqn1i];
         (* Not sure if the following context should not be used *)

--- a/quotient_def.ML	Wed Nov 18 23:52:48 2009 +0100
+++ b/quotient_def.ML	Thu Nov 19 14:17:10 2009 +0100
@@ -20,7 +20,7 @@
 fun define name mx attr rhs lthy =
 let
   val ((rhs, (_ , thm)), lthy') =
-     LocalTheory.define Thm.internalK ((name, mx), (attr, rhs)) lthy
+     Local_Theory.define "" ((name, mx), (attr, rhs)) lthy
 in
   ((rhs, thm), lthy')
 end
@@ -140,7 +140,7 @@
 
   val nconst_str = Binding.name_of nconst_bname
   val qcinfo = {qconst = trm, rconst = rhs}
-  val lthy'' = LocalTheory.declaration true
+  val lthy'' = Local_Theory.declaration true
                 (fn phi => qconsts_update_generic nconst_str 
                              (qconsts_transfer phi qcinfo)) lthy'
 in
@@ -159,7 +159,7 @@
 
 fun quotdef ((bind, qty, mx), (attr, prop)) lthy =
 let   
-  val (_, prop') = Primitive_Defs.dest_def lthy (K true) (K false) (K false) prop
+  val (_, prop') = LocalDefs.cert_def lthy prop
   val (_, rhs) = Primitive_Defs.abs_def prop'
 in
   make_def bind qty mx attr rhs lthy