src/Pure/Isar/proof_context.ML

   Ctxt {mode = mode, naming = naming, syntax = syntax,
     consts = consts, facts = facts, cases = cases};
 
 val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
 
-structure ContextData = ProofDataFun
+structure ContextData = Proof_Data
 (
   type T = ctxt;
   fun init thy =
     make_ctxt (mode_default, local_naming, Local_Syntax.init thy,
       (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []);

   in T end;
 
 
 local
 
-structure Allow_Dummies = ProofDataFun(type T = bool fun init _ = false);
+structure Allow_Dummies = Proof_Data(type T = bool fun init _ = false);
 
 fun check_dummies ctxt t =
   if Allow_Dummies.get ctxt then t
   else Term.no_dummy_patterns t handle TERM _ => error "Illegal dummy pattern(s) in term";