tuned;

--- a/src/Pure/Isar/rule_cases.ML	Sat Feb 11 17:17:45 2006 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Sat Feb 11 17:17:47 2006 +0100
@@ -81,12 +81,12 @@
 
 fun extract_fixes NONE prop = (strip_params prop, [])
   | extract_fixes (SOME outline) prop =
-      splitAt (length (Logic.strip_params outline), strip_params prop);
+      chop (length (Logic.strip_params outline)) (strip_params prop);
 
 fun extract_assumes _ NONE prop = ([("", Logic.strip_assums_hyp prop)], [])
   | extract_assumes qual (SOME outline) prop =
       let val (hyps, prems) =
-        splitAt (length (Logic.strip_assums_hyp outline), Logic.strip_assums_hyp prop)
+        chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
       in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end;
 
 fun extract_case is_open thy (case_outline, raw_prop) name concls =

--- a/src/Pure/Syntax/syn_ext.ML	Sat Feb 11 17:17:45 2006 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Sat Feb 11 17:17:47 2006 +0100
@@ -298,7 +298,7 @@
             err_in_mfix "Missing structure argument for indexed syntax" mfix;
 
           val xs = map Ast.Variable (Term.invent_names [] "xa" (length args - 1));
-          val (xs1, xs2) = Library.splitAt (Library.find_index is_index args, xs);
+          val (xs1, xs2) = chop (find_index is_index args) xs;
           val i = Ast.Variable "i";
           val lhs = Ast.mk_appl (Ast.Constant indexed_const)
             (xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2);

--- a/src/Pure/Thy/thm_database.ML	Sat Feb 11 17:17:45 2006 +0100
+++ b/src/Pure/Thy/thm_database.ML	Sat Feb 11 17:17:47 2006 +0100
@@ -92,7 +92,7 @@
           else NONE;
         val names = NameSpace.unpack name;
       in
-        (case #2 (splitAt (length names - 2, names)) of
+        (case #2 (chop (length names - 2) names) of
           [bname] => result "" bname
         | [prfx, bname] => result (if prfx = thy_name then "" else prfx) bname
         | _ => NONE)

--- a/src/Pure/proofterm.ML	Sat Feb 11 17:17:45 2006 +0100
+++ b/src/Pure/proofterm.ML	Sat Feb 11 17:17:47 2006 +0100
@@ -913,7 +913,7 @@
             val prop = (case prf of PThm (_, _, prop, _) => prop | PAxm (_, prop, _) => prop
               | Oracle (_, prop, _) => prop | _ => error "shrink: proof not in normal form");
             val vs = vars_of prop;
-            val (ts', ts'') = splitAt (length vs, ts)
+            val (ts', ts'') = chop (length vs) ts;
             val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts';
             val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
               insert (op =) ixn (case AList.lookup (op =) insts ixn of

--- a/src/Pure/thm.ML	Sat Feb 11 17:17:45 2006 +0100
+++ b/src/Pure/thm.ML	Sat Feb 11 17:17:47 2006 +0100
@@ -1219,7 +1219,7 @@
     val Bi' =
       if 0 = m orelse m = n then Bi
       else if 0 < m andalso m < n then
-        let val (ps, qs) = splitAt (m, asms)
+        let val (ps, qs) = chop m asms
         in list_all (params, Logic.list_implies (qs @ ps, concl)) end
       else raise THM ("rotate_rule", k, [state]);
   in
@@ -1249,7 +1249,7 @@
     val prop' =
       if 0 = m orelse m = n_j then prop
       else if 0 < m andalso m < n_j then
-        let val (ps, qs) = splitAt (m, moved_prems)
+        let val (ps, qs) = chop m moved_prems
         in Logic.list_implies (fixed_prems @ qs @ ps, concl) end
       else raise THM ("permute_prems: k", k, [rl]);
   in

--- a/src/Pure/type_infer.ML	Sat Feb 11 17:17:45 2006 +0100
+++ b/src/Pure/type_infer.ML	Sat Feb 11 17:17:47 2006 +0100
@@ -342,7 +342,7 @@
     fun prep_output bs ts Ts =
       let
         val (Ts_bTs', ts') = typs_terms_of [] PTFree "??" (Ts @ map snd bs, ts);
-        val (Ts',Ts'') = Library.splitAt(length Ts, Ts_bTs');
+        val (Ts', Ts'') = chop (length Ts) Ts_bTs';
         val xs = map Free (map fst bs ~~ Ts'');
         val ts'' = map (fn t => subst_bounds (xs, t)) ts';
       in (ts'', Ts') end;