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