1.1 --- a/src/Pure/Isar/proof_context.ML	Sun Nov 08 16:28:18 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Nov 08 16:30:41 2009 +0100
     1.3 @@ -177,7 +177,7 @@
     1.4  
     1.5  val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
     1.6  
     1.7 -structure ContextData = ProofDataFun
     1.8 +structure ContextData = Proof_Data
     1.9  (
    1.10    type T = ctxt;
    1.11    fun init thy =
    1.12 @@ -515,7 +515,7 @@
    1.13  
    1.14  local
    1.15  
    1.16 -structure Allow_Dummies = ProofDataFun(type T = bool fun init _ = false);
    1.17 +structure Allow_Dummies = Proof_Data(type T = bool fun init _ = false);
    1.18  
    1.19  fun check_dummies ctxt t =
    1.20    if Allow_Dummies.get ctxt then t