src/Pure/Isar/attrib.ML
changeset 35021 c839a4c670c6
parent 34986 7f7939c9370f
child 35624 c4e29a0bb8c1
     1.1 --- a/src/Pure/Isar/attrib.ML	Sun Feb 07 19:31:55 2010 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sun Feb 07 19:33:34 2010 +0100
     1.3 @@ -298,7 +298,7 @@
     1.4    setup (Binding.name "params")
     1.5      (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
     1.6      "named rule parameters" #>
     1.7 -  setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.standard)))
     1.8 +  setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.export_without_context)))
     1.9      "result put into standard form (legacy)" #>
    1.10    setup (Binding.name "rule_format") rule_format "result put into canonical rule format" #>
    1.11    setup (Binding.name "elim_format") (Scan.succeed elim_format)