changed order of arguments to "bnf_sugar"
authorblanchet
Thu, 30 Aug 2012 09:47:46 +0200
changeset 49023 5afe918dd476
parent 49022 005ce926a932
child 49024 224a0c63ba23
changed order of arguments to "bnf_sugar"
src/HOL/Codatatype/Tools/bnf_sugar.ML
--- 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;