# HG changeset patch
# User blanchet
# Date 1346312866 -7200
# Node ID 5afe918dd476cffff5ad83fab53a538e583f2836
# Parent  005ce926a932859811c00156614fc01deb5d1883
changed order of arguments to "bnf_sugar"

diff -r 005ce926a932 -r 5afe918dd476 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;