src/Pure/Proof/extraction.ML
changeset 26463 9283b4185fdf
parent 26435 bdce320cd426
child 26481 92e901171cc8
     1.1 --- a/src/Pure/Proof/extraction.ML	Fri Mar 28 19:43:54 2008 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Fri Mar 28 20:02:04 2008 +0100
     1.3 @@ -395,7 +395,7 @@
     1.4  
     1.5  (** Pure setup **)
     1.6  
     1.7 -val _ = Context.>>
     1.8 +val _ = Context.>> (Context.map_theory
     1.9    (add_types [("prop", ([], NONE))] #>
    1.10  
    1.11     add_typeof_eqns
    1.12 @@ -441,7 +441,7 @@
    1.13  
    1.14     Attrib.add_attributes
    1.15       [("extraction_expand", extraction_expand,
    1.16 -       "specify theorems / definitions to be expanded during extraction")]);
    1.17 +       "specify theorems / definitions to be expanded during extraction")]));
    1.18  
    1.19  
    1.20  (**** extract program ****)