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