changeset 20897 | 3f8d2834b2c4 |
parent 20854 | f9cf9e62d11c |
child 21646 | c07b5b0e8492 |
--- a/src/Pure/Proof/extraction.ML Sat Oct 07 07:41:56 2006 +0200 +++ b/src/Pure/Proof/extraction.ML Mon Oct 09 02:19:49 2006 +0200 @@ -384,7 +384,7 @@ val add_expand_thms = fold add_expand_thm; val extraction_expand = - Attrib.no_args (Thm.declaration_attribute (Context.map_theory o add_expand_thm)); + Attrib.no_args (Thm.declaration_attribute (fn th => Context.mapping (add_expand_thm th) I)); (** types with computational content **)