# HG changeset patch
# User haftmann
# Date 1135167920 -3600
# Node ID e57731ba01dd75c6b246717da9b71fd334ce007d
# Parent  e314fb38307da34c3470ebff495325324f8b0f81
discontinued unflat in favour of burrow and burrow_split

diff -r e314fb38307d -r e57731ba01dd NEWS
--- a/NEWS	Wed Dec 21 12:06:08 2005 +0100
+++ b/NEWS	Wed Dec 21 13:25:20 2005 +0100
@@ -163,6 +163,20 @@
 
 *** ML ***
 
+* Pure/library:
+
+  val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
+  val burrow_split: ('a list -> 'c * 'b list) -> 'a list list -> 'c * 'b list list
+
+The semantics of "burrow" is: "take a function with *simulatanously* transforms
+a list of value, and apply it *simulatanously* to a list of list of values of the
+appropriate type". Confer this with "map" which would *not* apply its argument
+function simulatanously but in sequence. "burrow_split" allows the transformator
+function to yield an additional side result.
+
+Both actually avoid the usage of "unflat" since they hide away "unflat"
+from the user.
+
 * Pure/library: functions map2 and fold2 with curried syntax for
 simultanous mapping and folding:
 
diff -r e314fb38307d -r e57731ba01dd src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Dec 21 12:06:08 2005 +0100
+++ b/src/Pure/Isar/locale.ML	Wed Dec 21 13:25:20 2005 +0100
@@ -1201,24 +1201,21 @@
        the fixes elements in raw_elemss,
        raw_proppss contains assumptions and definitions from the
        external elements in raw_elemss. *)
-    val raw_propps = map List.concat raw_proppss;
-    val raw_propp = List.concat raw_propps;
+    fun prep_prop raw_ctxt raw_concl raw_propp =
+      let
+        (* CB: add type information from fixed_params to context (declare_term) *)
+        (* CB: process patterns (conclusion and external elements only) *)
+        val (ctxt, all_propp) =
+          prepp (fold ProofContext.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
+        (* CB: add type information from conclusion and external elements to context *)
+        val ctxt = fold ProofContext.declare_term (List.concat (map (map fst) all_propp)) ctxt;
+        (* CB: resolve schematic variables (patterns) in conclusion and external elements. *)
+        val all_propp' = map2 (curry (op ~~))
+          (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
+        val (concl, propp) = splitAt (length raw_concl, all_propp')
+      in ((ctxt, concl), propp) end
 
-    (* CB: add type information from fixed_params to context (declare_term) *)
-    (* CB: process patterns (conclusion and external elements only) *)
-    val (ctxt, all_propp) =
-      prepp (fold ProofContext.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
-    (* CB: add type information from conclusion and external elements
-       to context *)
-    val ctxt = fold ProofContext.declare_term (List.concat (map (map fst) all_propp)) ctxt;
-
-    (* CB: resolve schematic variables (patterns) in conclusion and external
-       elements. *)
-    val all_propp' = map2 (curry (op ~~))
-      (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
-    val (concl, propp) = splitAt(length raw_concl, all_propp');
-    val propps = unflat raw_propps propp;
-    val proppss = map (uncurry unflat) (raw_proppss ~~ propps);
+    val ((ctxt, concl), proppss) = (burrow_split o burrow_split) (prep_prop raw_ctxt raw_concl) raw_proppss;
 
     (* CB: obtain all parameters from identifier part of raw_elemss *)
     val xs = map #1 (params_of' raw_elemss);
diff -r e314fb38307d -r e57731ba01dd src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Dec 21 12:06:08 2005 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Dec 21 13:25:20 2005 +0100
@@ -801,12 +801,12 @@
     val outer_state = state |> close_block;
     val outer_ctxt = context_of outer_state;
 
-    val raw_props = List.concat stmt;
+    val raw_props = Library.flat stmt;
     val props = ProofContext.generalize goal_ctxt outer_ctxt raw_props;
     val results =
-      conclude_goal state raw_props goal
-      |> Seq.map_list (ProofContext.exports goal_ctxt outer_ctxt)
-      |> Seq.map (Library.unflat stmt);
+      stmt
+      |> burrow (fn raw_props => conclude_goal state raw_props goal)
+      |> (Seq.map_list o Seq.map_list) (ProofContext.exports goal_ctxt outer_ctxt);
   in
     outer_state
     |> map_context (ProofContext.auto_bind_facts props)
diff -r e314fb38307d -r e57731ba01dd src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Dec 21 12:06:08 2005 +0100
+++ b/src/Pure/library.ML	Wed Dec 21 13:25:20 2005 +0100
@@ -102,7 +102,7 @@
   val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
   val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
   val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
-  val unflat: 'a list list -> 'b list -> 'b list list
+  val burrow_split: ('a list -> 'c * 'b list) -> 'a list list -> 'c * 'b list list
   val splitAt: int * 'a list -> 'a list * 'a list
   val dropwhile: ('a -> bool) -> 'a list -> 'a list
   val nth: 'a list -> int -> 'a
@@ -599,6 +599,8 @@
 fun burrow f xss =
   unflat xss ((f o flat) xss);
 
+fun burrow_split f xss =
+  apsnd (unflat xss) ((f o flat) xss);
 
 (*like Lisp's MAPC -- seq proc [x1, ..., xn] evaluates
   (proc x1; ...; proc xn) for side effects*)