--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Sat Jun 11 13:57:59 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Sat Jun 11 16:41:11 2016 +0200
@@ -2394,13 +2394,13 @@
val _ = Outer_Syntax.local_theory @{command_keyword corec}
"define nonprimitive corecursive functions"
((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
- --| @{keyword ")"}) []) -- (Parse.fixes --| Parse.where_ -- Parse.prop)
+ --| @{keyword ")"}) []) -- (Parse.vars --| Parse.where_ -- Parse.prop)
>> uncurry corec_cmd);
val _ = Outer_Syntax.local_theory_to_proof @{command_keyword corecursive}
"define nonprimitive corecursive functions"
((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
- --| @{keyword ")"}) []) -- (Parse.fixes --| Parse.where_ -- Parse.prop)
+ --| @{keyword ")"}) []) -- (Parse.vars --| Parse.where_ -- Parse.prop)
>> uncurry corecursive_cmd);
val _ = Outer_Syntax.local_theory_to_proof @{command_keyword friend_of_corec}