# HG changeset patch
# User blanchet
# Date 1349035354 -7200
# Node ID 0209087a14d056b3a8e9fa3b33a4cbc67ef2e607
# Parent  44d85dc8ca08b35b18b77b4c889ae7c81080b5fc
tuning

diff -r 44d85dc8ca08 -r 0209087a14d0 src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Sun Sep 30 12:08:16 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Sun Sep 30 22:02:34 2012 +0200
@@ -51,6 +51,12 @@
     fold_rev (fn T => fn t => Abs (Name.uu, T, t)) binders (Bound (length binders - k))
   end;
 
+fun hhf_concl_conv cv ctxt ct =
+  (case Thm.term_of ct of
+    Const (@{const_name all}, _) $ Abs _ =>
+    Conv.arg_conv (Conv.abs_conv (hhf_concl_conv cv o snd) ctxt) ct
+  | _ => Conv.concl_conv ~1 cv ct);
+
 fun inst_as_projs ctxt k thm =
   let
     val fs =
@@ -141,15 +147,6 @@
       pre_set_defss mss (unflat mss (1 upto n)) kkss)
   end;
 
-local
-
-fun hhf_concl_conv cv ctxt ct =
-  (case Thm.term_of ct of
-    Const ("all", _) $ Abs _ => Conv.arg_conv (Conv.abs_conv (hhf_concl_conv cv o snd) ctxt) ct
-  | _ => Conv.concl_conv ~1 cv ct);
-
-in
-
 fun mk_coinduct_same_ctr ctxt rel_eqs pre_rel_def dtor_ctor ctr_def discs sels =
   hyp_subst_tac THEN'
   CONVERSION (hhf_concl_conv
@@ -161,8 +158,6 @@
        (ss_only (@{thm prod.inject} :: no_refl discs @ rel_eqs @ more_simp_thms)) THEN_MAYBE'
      REPEAT o hyp_subst_tac THEN' REPEAT o rtac conjI THEN' REPEAT o rtac refl);
 
-end;
-
 fun mk_coinduct_distinct_ctrs discs discs' =
   hyp_subst_tac THEN' REPEAT o etac conjE THEN'
   full_simp_tac (ss_only (refl :: no_refl (discs @ discs') @ basic_simp_thms));
diff -r 44d85dc8ca08 -r 0209087a14d0 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Sun Sep 30 12:08:16 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Sun Sep 30 22:02:34 2012 +0200
@@ -2698,7 +2698,7 @@
                 Thm.instantiate (Tinst, []) o Drule.zero_var_indexes))
               dtors set_incl_hset_thmss;
 
-            val tinst = interleave (map (SOME o certify lthy) dtors) (replicate n NONE)
+            val tinst = splice (map (SOME o certify lthy) dtors) (replicate n NONE)
             val set_minimal_thms =
               map (Drule.instantiate' [] tinst o Thm.instantiate (Tinst, []) o
                 Drule.zero_var_indexes)
diff -r 44d85dc8ca08 -r 0209087a14d0 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Sun Sep 30 12:08:16 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Sun Sep 30 22:02:34 2012 +0200
@@ -1625,7 +1625,7 @@
         val map_wpull_thms =
           let
             val cTs = map (SOME o certifyT lthy o TFree) induct2_params;
-            val cxs = map (SOME o certify lthy) (interleave Izs1 Izs2);
+            val cxs = map (SOME o certify lthy) (splice Izs1 Izs2);
 
             fun mk_prem z1 z2 sets1 sets2 map1 map2 =
               HOLogic.mk_conj
diff -r 44d85dc8ca08 -r 0209087a14d0 src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Sun Sep 30 12:08:16 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Sun Sep 30 22:02:34 2012 +0200
@@ -40,7 +40,7 @@
     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g -> 'h list * 'g
   val fold_map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i * 'h) ->
     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h -> 'i list * 'h
-  val interleave: 'a list -> 'a list -> 'a list
+  val splice: 'a list -> 'a list -> 'a list
   val transpose: 'a list list -> 'a list list
   val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list
 
@@ -602,7 +602,7 @@
     | mk_UnIN n m = mk_UnIN' (n - m)
 end;
 
-fun interleave xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys);
+fun splice xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys);
 
 fun transpose [] = []
   | transpose ([] :: xss) = transpose xss
diff -r 44d85dc8ca08 -r 0209087a14d0 src/HOL/BNF/Tools/bnf_wrap.ML
--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Sun Sep 30 12:08:16 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Sun Sep 30 22:02:34 2012 +0200
@@ -80,7 +80,7 @@
     val xsss =
       map2 (map2 append) (Library.chop_groups n half_xss)
         (transpose (Library.chop_groups n other_half_xss))
-    val xs = interleave (flat half_xss) (flat other_half_xss);
+    val xs = splice (flat half_xss) (flat other_half_xss);
   in (xs, xsss) end;
 
 fun mk_undefined T = Const (@{const_name undefined}, T);