src/Pure/Isar/proof.ML

     state
     |> map_context_result (prep_vars (map (fn (x, mx) => (x, NONE, mx)) raw_vars))
     |>> map (fn (x, _, mx) => (x, mx))
     |-> (fn vars =>
       map_context_result (prep_binds false (map swap raw_rhss))
-      #-> (fn rhss => map_context_result (LocalDefs.add_defs (vars ~~ (name_atts ~~ rhss)))))
+      #-> (fn rhss => map_context_result (Local_Defs.add_defs (vars ~~ (name_atts ~~ rhss)))))
     |-> (put_facts o SOME o map (#2 o #2))
   end;
 
 in
 

         val ctxt = context_of state';
         val ths = maps snd named_facts;
       in (statement, [], f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end));
 
 fun append_using _ ths using = using @ filter_out Thm.is_dummy ths;
-fun unfold_using ctxt ths = map (LocalDefs.unfold ctxt ths);
-val unfold_goals = LocalDefs.unfold_goals;
+fun unfold_using ctxt ths = map (Local_Defs.unfold ctxt ths);
+val unfold_goals = Local_Defs.unfold_goals;
 
 in
 
 val using = gen_using append_using (K (K I)) Attrib.attribute ProofContext.get_fact;
 val using_i = gen_using append_using (K (K I)) (K I) (K I);