# HG changeset patch
# User blanchet
# Date 1473101827 -7200
# Node ID dbda3556d495e068e073f4a6e23ecf42f0c626e1
# Parent  45c8762353dd2e3a484509f6a7999409de6e2c1a
exported ML functions

diff -r 45c8762353dd -r dbda3556d495 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 05 18:40:29 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 05 20:57:07 2016 +0200
@@ -473,11 +473,6 @@
       | zed xs (y :: ys) = f (xs, y, ys) :: zed (xs @ [y]) ys;
   in zed [] end;
 
-fun unfla xs = fold_map (fn _ => fn (c :: cs) => (c, cs)) xs;
-fun unflat xss = fold_map unfla xss;
-fun unflatt xsss = fold_map unflat xsss;
-fun unflattt xssss = fold_map unflatt xssss;
-
 fun cannot_merge_types fp =
   error ("Mutually " ^ co_prefix fp ^ "recursive types must have the same type parameters");
 
@@ -894,7 +889,7 @@
                 end) setAs lthy;
             val goals = flat (flat (flat goalssss));
           in
-            `(fst o unflattt goalssss)
+            `(unflattt goalssss)
               (if null goals then []
                else
                  let
@@ -1043,7 +1038,7 @@
             val goalss = @{map 3} (map2 o mk_goal) discAs selAss selBss;
             val goals = flat goalss;
           in
-            `(fst o unflat goalss)
+            `(unflat goalss)
               (if null goals then []
               else
                 let
@@ -1106,7 +1101,7 @@
                 setAs names_lthy;
             val goals = flat (flat (flat goalssss));
           in
-            `(fst o unflattt goalssss)
+            `(unflattt goalssss)
               (if null goals then []
               else
                 let
diff -r 45c8762353dd -r dbda3556d495 src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Sep 05 18:40:29 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Mon Sep 05 20:57:07 2016 +0200
@@ -10,6 +10,9 @@
   include CTR_SUGAR_UTIL
   include BNF_FP_REC_SUGAR_UTIL
 
+  val unflatt: 'a list list list -> 'b list -> 'b list list list
+  val unflattt: 'a list list list list -> 'b list -> 'b list list list list
+
   val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context
   val mk_Freesss: string -> typ list list list -> Proof.context ->
     term list list list * Proof.context
@@ -117,6 +120,14 @@
 
 (* Library proper *)
 
+fun unfla0 xs = fold_map (fn _ => fn (c :: cs) => (c, cs)) xs;
+fun unflat0 xss = fold_map unfla0 xss;
+fun unflatt0 xsss = fold_map unflat0 xsss;
+fun unflattt0 xssss = fold_map unflatt0 xssss;
+
+fun unflatt xsss = fst o unflatt0 xsss;
+fun unflattt xssss = fst o unflattt0 xssss;
+
 val parse_type_arg_constrained =
   Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);