--- a/src/Pure/Isar/attrib.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Pure/Isar/attrib.ML Sun Nov 01 15:24:45 2009 +0100
@@ -287,15 +287,15 @@
"rename bound variables in abstractions" #>
setup (Binding.name "unfolded") unfolded "unfolded definitions" #>
setup (Binding.name "folded") folded "folded definitions" #>
- setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> RuleCases.consumes)
+ setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> Rule_Cases.consumes)
"number of consumed facts" #>
- setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names)
+ setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> Rule_Cases.case_names)
"named rule cases" #>
setup (Binding.name "case_conclusion")
- (Scan.lift (Args.name -- Scan.repeat Args.name) >> RuleCases.case_conclusion)
+ (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
"named conclusion of rule cases" #>
setup (Binding.name "params")
- (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> RuleCases.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)))
"result put into standard form (legacy)" #>