src/Pure/Proof/extraction.ML

     thy;
 
 
 (** Pure setup **)
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
   (add_types [("prop", ([], NONE))] #>
 
    add_typeof_eqns
      ["(typeof (PROP P)) == (Type (TYPE(Null))) ==>  \
     \  (typeof (PROP Q)) == (Type (TYPE('Q))) ==>  \

     \  (!!x. PROP realizes (r (x)) (PROP P (x)))"] #>
 
    Attrib.setup (Binding.name "extraction_expand") (Scan.succeed (extraction_expand false))
      "specify theorems to be expanded during extraction" #>
    Attrib.setup (Binding.name "extraction_expand_def") (Scan.succeed (extraction_expand true))
-     "specify definitions to be expanded during extraction"));
+     "specify definitions to be expanded during extraction");
 
 
 (**** extract program ****)
 
 val dummyt = Const ("dummy", dummyT);