src/Pure/Isar/attrib.ML
changeset 33368 b1cf34f1855c
parent 33159 369da293bbd4
child 33522 737589bb9bb8
     1.1 --- a/src/Pure/Isar/attrib.ML	Fri Oct 30 18:33:21 2009 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sun Nov 01 15:24:45 2009 +0100
     1.3 @@ -287,15 +287,15 @@
     1.4      "rename bound variables in abstractions" #>
     1.5    setup (Binding.name "unfolded") unfolded "unfolded definitions" #>
     1.6    setup (Binding.name "folded") folded "folded definitions" #>
     1.7 -  setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> RuleCases.consumes)
     1.8 +  setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> Rule_Cases.consumes)
     1.9      "number of consumed facts" #>
    1.10 -  setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names)
    1.11 +  setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> Rule_Cases.case_names)
    1.12      "named rule cases" #>
    1.13    setup (Binding.name "case_conclusion")
    1.14 -    (Scan.lift (Args.name -- Scan.repeat Args.name) >> RuleCases.case_conclusion)
    1.15 +    (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
    1.16      "named conclusion of rule cases" #>
    1.17    setup (Binding.name "params")
    1.18 -    (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> RuleCases.params)
    1.19 +    (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
    1.20      "named rule parameters" #>
    1.21    setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.standard)))
    1.22      "result put into standard form (legacy)" #>