src/Pure/pure_thy.ML

 
 (*** stored facts ***)
 
 (** theory data **)
 
-structure FactsData = TheoryDataFun
+structure FactsData = Theory_Data
 (
   type T = Facts.T * thm list;
   val empty = (Facts.empty, []);
-  val copy = I;
   fun extend (facts, _) = (facts, []);
-  fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
+  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
 );
 
 
 (* facts *)
 

  [("",       typ "'a => cargs",                  Delimfix "_"),
   ("_cargs", typ "'a => cargs => cargs",         Mixfix ("_/ _", [1000, 1000], 1000)),
   ("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)),
   ("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))];
 
-structure OldApplSyntax = TheoryDataFun
+structure OldApplSyntax = Theory_Data
 (
   type T = bool;
   val empty = false;
-  val copy = I;
   val extend = I;
-  fun merge _ (b1, b2) : T =
+  fun merge (b1, b2) : T =
     if b1 = b2 then b1
     else error "Cannot merge theories with different application syntax";
 );
 
 val old_appl_syntax = OldApplSyntax.get;

 
 (* main content *)
 
 val _ = Context.>> (Context.map_theory
   (Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
-   OldApplSyntax.init #>
+   OldApplSyntax.put false #>
    Sign.add_types
    [(Binding.name "fun", 2, NoSyn),
     (Binding.name "prop", 0, NoSyn),
     (Binding.name "itself", 1, NoSyn),
     (Binding.name "dummy", 0, NoSyn)]