--- a/src/HOL/Codatatype/Tools/bnf_sugar.ML Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML Thu Aug 30 09:47:46 2012 +0200
@@ -18,7 +18,7 @@
val distinctN = "distinct";
-fun prepare_sugar prep_term (((raw_ctors, dtor_names), stor_namess), raw_caseof) no_defs_lthy =
+fun prepare_sugar prep_term (((raw_ctors, raw_caseof), dtor_names), stor_namess) no_defs_lthy =
let
(* TODO: sanity checks on arguments *)
@@ -147,8 +147,8 @@
val _ =
Outer_Syntax.local_theory_to_proof @{command_spec "bnf_sugar"} "adds sugar on top of a BNF"
- (((Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") --
- parse_binding_list -- (Parse.$$$ "[" |-- Parse.list parse_binding_list --| Parse.$$$ "]") --
- Parse.term) >> bnf_sugar_cmd);
+ (((Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- Parse.term --
+ parse_binding_list -- (Parse.$$$ "[" |-- Parse.list parse_binding_list --| Parse.$$$ "]"))
+ >> bnf_sugar_cmd);
end;