--- a/src/Pure/Isar/attrib.ML Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Pure/Isar/attrib.ML Sun Feb 07 19:33:34 2010 +0100
@@ -298,7 +298,7 @@
setup (Binding.name "params")
(Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
"named rule parameters" #>
- setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.standard)))
+ setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.export_without_context)))
"result put into standard form (legacy)" #>
setup (Binding.name "rule_format") rule_format "result put into canonical rule format" #>
setup (Binding.name "elim_format") (Scan.succeed elim_format)