src/HOL/Tools/split_rule.ML

 
 
 (* complete splitting of partially splitted rules *)
 
 fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
-      (ap_split T (flat (map HOLogic.prodT_factors Ts) ---> U)
+      (ap_split T (List.concat (map HOLogic.prodT_factors Ts) ---> U)
         (incr_boundvars 1 u) $ Bound 0))
   | ap_split' _ _ u = u;
 
 fun complete_split_rule_var ((t as Var (v, T), ts), (rl, vs)) =
       let
         val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl))
         val (Us', U') = strip_type T;
-        val Us = take (length ts, Us');
-        val U = drop (length ts, Us') ---> U';
-        val T' = flat (map HOLogic.prodT_factors Us) ---> U;
+        val Us = Library.take (length ts, Us');
+        val U = Library.drop (length ts, Us') ---> U';
+        val T' = List.concat (map HOLogic.prodT_factors Us) ---> U;
         fun mk_tuple ((xs, insts), v as Var ((a, _), T)) =
               let
                 val Ts = HOLogic.prodT_factors T;
                 val ys = Term.variantlist (replicate (length Ts) a, xs);
               in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
                 (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
               end
           | mk_tuple (x, _) = x;
         val newt = ap_split' Us U (Var (v, T'));
         val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl));
-        val (vs', insts) = foldl mk_tuple ((vs, []), ts);
+        val (vs', insts) = Library.foldl mk_tuple ((vs, []), ts);
       in
         (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
       end
   | complete_split_rule_var (_, x) = x;
 
 fun collect_vars (vs, Abs (_, _, t)) = collect_vars (vs, t)
   | collect_vars (vs, t) = (case strip_comb t of
         (v as Var _, ts) => (v, ts)::vs
-      | (t, ts) => foldl collect_vars (vs, ts));
+      | (t, ts) => Library.foldl collect_vars (vs, ts));
 
 
 val split_rule_var = Drule.standard o remove_internal_split o split_rule_var';
 
 (*curries ALL function variables occurring in a rule's conclusion*)
 fun split_rule rl =
-  foldr split_rule_var' (Term.term_vars (concl_of rl), rl)
+  Library.foldr split_rule_var' (Term.term_vars (concl_of rl), rl)
   |> remove_internal_split
   |> Drule.standard;
 
 fun complete_split_rule rl =
-  fst (foldr complete_split_rule_var
+  fst (Library.foldr complete_split_rule_var
     (collect_vars ([], concl_of rl),
       (rl, map (fst o fst o dest_Var) (Term.term_vars (#prop (Thm.rep_thm rl))))))
   |> remove_internal_split
   |> Drule.standard
   |> RuleCases.save rl;

 val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv];
 
 fun split_rule_goal xss rl =
   let
     fun one_split i (th, s) = Tactic.rule_by_tactic (pair_tac s i) th;
-    fun one_goal (xs, i) th = foldl (one_split i) (th, xs);
+    fun one_goal (xs, i) th = Library.foldl (one_split i) (th, xs);
   in
     Drule.standard (Simplifier.full_simplify split_rule_ss (Library.foldln one_goal xss rl))
     |> RuleCases.save rl
   end;