--- a/Attic/Quot/quotient_def.ML	Thu Mar 04 15:56:58 2010 +0100
+++ b/Attic/Quot/quotient_def.ML	Sun Mar 07 21:30:12 2010 +0100
@@ -63,7 +63,7 @@
   val qconst_bname = Binding.name lhs_str
   val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
   val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
-  val (_, prop') = LocalDefs.cert_def lthy prop
+  val (_, prop') = Local_Defs.cert_def lthy prop
   val (_, newrhs) = Primitive_Defs.abs_def prop'
 
   val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy

--- a/Attic/Quot/quotient_tacs.ML	Thu Mar 04 15:56:58 2010 +0100
+++ b/Attic/Quot/quotient_tacs.ML	Sun Mar 07 21:30:12 2010 +0100
@@ -48,7 +48,7 @@
 fun atomize_thm thm =
 let
   val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
-  val thm'' = ObjectLogic.atomize (cprop_of thm')
+  val thm'' = Object_Logic.atomize (cprop_of thm')
 in
   @{thm equal_elim_rule1} OF [thm'', thm']
 end
@@ -616,7 +616,7 @@
 
 (* the tactic leaves three subgoals to be proved *)
 fun procedure_tac ctxt rthm =
-  ObjectLogic.full_atomize_tac
+  Object_Logic.full_atomize_tac
   THEN' gen_frees_tac ctxt
   THEN' SUBGOAL (fn (goal, i) =>
     let