src/Pure/pure_thy.ML

      (ref (Thms {theorems = _, all_facts = all_facts1}),
       ref (Thms {theorems = _, all_facts = all_facts2})) =
     ref (make_thms NameSpace.empty_table (Facts.merge (all_facts1, all_facts2)));
 );
 
-val _ = Context.>> TheoremsData.init;
+val _ = Context.>> (Context.map_theory TheoremsData.init);
 
 val get_theorems_ref = TheoremsData.get;
 val get_theorems = (fn Thms args => args) o ! o get_theorems_ref;
 val theorems_of = #theorems o get_theorems;
 val all_facts_of = #all_facts o get_theorems;

 
 val typ = SimpleSyntax.read_typ;
 val term = SimpleSyntax.read_term;
 val prop = SimpleSyntax.read_prop;
 
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
   (Sign.add_types
    [("fun", 2, NoSyn),
     ("prop", 0, NoSyn),
     ("itself", 1, NoSyn),
     ("dummy", 0, NoSyn)]

    [("prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
     ("term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
     ("conjunction_def", prop "(A && B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
   #> Sign.hide_consts false ["conjunction", "term"]
   #> add_thmss [(("nothing", []), [])] #> snd
-  #> Theory.add_axioms_i Proofterm.equality_axms);
+  #> Theory.add_axioms_i Proofterm.equality_axms));
 
 end;