# HG changeset patch
# User blanchet
# Date 1413453406 -7200
# Node ID 15e5b44d5ed23d16b419625ea0b4077a3546a33e
# Parent  6a75a4c24339df7d26f1b4177f7ecddcadee888d
made SML/NJ happier

diff -r 6a75a4c24339 -r 15e5b44d5ed2 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Oct 15 17:18:08 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Oct 16 11:56:46 2014 +0200
@@ -415,16 +415,16 @@
 fun zipper_map f =
   let
     fun zed _ [] = []
-      | zed xs (y :: ys) = f (xs, y, ys) :: zed (xs @ [y]) ys
+      | zed xs (y :: ys) = f (xs, y, ys) :: zed (xs @ [y]) ys;
   in zed [] end;
 
-val unfla = fold_map (fn _ => fn y :: ys => (y, ys))
-val unflat = fold_map unfla
-val unflatt = fold_map unflat
-val unflattt = fold_map unflatt
+fun unfla _ = rpair [];
+fun unflat xss = fold_map unfla xss;
+fun unflatt xsss = fold_map unflat xsss;
+fun unflattt xssss = fold_map unflatt xssss;
 
 fun ctr_sugar_kind_of_fp_kind Least_FP = Datatype
-  | ctr_sugar_kind_of_fp_kind Greatest_FP = Codatatype
+  | ctr_sugar_kind_of_fp_kind Greatest_FP = Codatatype;
 
 fun uncurry_thm 0 thm = thm
   | uncurry_thm 1 thm = thm