src/Pure/Proof/extraction.ML
changeset 26463 9283b4185fdf
parent 26435 bdce320cd426
child 26481 92e901171cc8
--- a/src/Pure/Proof/extraction.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Proof/extraction.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -395,7 +395,7 @@
 
 (** Pure setup **)
 
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
   (add_types [("prop", ([], NONE))] #>
 
    add_typeof_eqns
@@ -441,7 +441,7 @@
 
    Attrib.add_attributes
      [("extraction_expand", extraction_expand,
-       "specify theorems / definitions to be expanded during extraction")]);
+       "specify theorems / definitions to be expanded during extraction")]));
 
 
 (**** extract program ****)