--- a/src/HOL/Library/simps_case_conv.ML Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Library/simps_case_conv.ML Wed Apr 13 18:01:05 2016 +0200
@@ -231,15 +231,15 @@
val _ =
Outer_Syntax.local_theory @{command_keyword case_of_simps}
"turn a list of equations into a case expression"
- (Parse_Spec.opt_thm_name ":" -- Parse.xthms1 >> case_of_simps_cmd)
+ (Parse_Spec.opt_thm_name ":" -- Parse.thms1 >> case_of_simps_cmd)
val parse_splits = @{keyword "("} |-- Parse.reserved "splits" |-- @{keyword ":"} |--
- Parse.xthms1 --| @{keyword ")"}
+ Parse.thms1 --| @{keyword ")"}
val _ =
Outer_Syntax.local_theory @{command_keyword simps_of_case}
"perform case split on rule"
- (Parse_Spec.opt_thm_name ":" -- Parse.xthm --
+ (Parse_Spec.opt_thm_name ":" -- Parse.thm --
Scan.optional parse_splits [] >> simps_of_case_cmd)
end