src/Pure/Proof/extraction.ML
changeset 53171 a5e54d4d9081
parent 52788 da1fdbfebd39
child 56206 7adec2a527f5
     1.1 --- a/src/Pure/Proof/extraction.ML	Fri Aug 23 20:09:34 2013 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Fri Aug 23 20:35:50 2013 +0200
     1.3 @@ -422,7 +422,7 @@
     1.4  
     1.5  (** Pure setup **)
     1.6  
     1.7 -val _ = Context.>> (Context.map_theory
     1.8 +val _ = Theory.setup
     1.9    (add_types [("prop", ([], NONE))] #>
    1.10  
    1.11     add_typeof_eqns
    1.12 @@ -469,7 +469,7 @@
    1.13     Attrib.setup (Binding.name "extraction_expand") (Scan.succeed (extraction_expand false))
    1.14       "specify theorems to be expanded during extraction" #>
    1.15     Attrib.setup (Binding.name "extraction_expand_def") (Scan.succeed (extraction_expand true))
    1.16 -     "specify definitions to be expanded during extraction"));
    1.17 +     "specify definitions to be expanded during extraction");
    1.18  
    1.19  
    1.20  (**** extract program ****)