src/Pure/Isar/expression.ML

       in
         (case elem of
           Assumes asms => Assumes (asms |> map (fn (a, propps) =>
             (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
         | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) =>
-            let val ((c, _), t') = LocalDefs.cert_def ctxt (close_frees t)
+            let val ((c, _), t') = Local_Defs.cert_def ctxt (close_frees t)
             in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end))
         | e => e)
       end;
 
 fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>

 
 val norm_term = Envir.beta_norm oo Term.subst_atomic;
 
 fun bind_def ctxt eq (xs, env, eqs) =
   let
-    val _ = LocalDefs.cert_def ctxt eq;
-    val ((y, T), b) = LocalDefs.abs_def eq;
+    val _ = Local_Defs.cert_def ctxt eq;
+    val ((y, T), b) = Local_Defs.abs_def eq;
     val b' = norm_term env b;
     fun err msg = error (msg ^ ": " ^ quote y);
   in
     case filter (fn (Free (y', _), _) => y = y' | _ => false) env of
       [] => (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs) |

     fun note_eqns raw_eqns thy =
       let
         val eqns = map (Morphism.thm (export' $> export)) raw_eqns;
         val eqn_attrss = map2 (fn attrs => fn eqn =>
           ((apsnd o map) (Attrib.attribute_i thy) attrs, [([eqn], [])])) attrss eqns;
-        fun meta_rewrite thy = map (LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
-          Drule.abs_def) o maps snd;
+        fun meta_rewrite thy =
+          map (Local_Defs.meta_rewrite_rule (ProofContext.init thy) #> Drule.abs_def) o maps snd;
       in
         thy
         |> PureThy.note_thmss Thm.lemmaK eqn_attrss
         |-> (fn facts => `(fn thy => meta_rewrite thy facts))
       end;