tuned;
authorwenzelm
Sat Feb 11 17:17:47 2006 +0100 (2006-02-11)
changeset 190122577ac76cdc6
parent 19011 d1c3294ca417
child 19013 19ad0c59fb1f
tuned;
src/Pure/Isar/rule_cases.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Thy/thm_database.ML
src/Pure/proofterm.ML
src/Pure/thm.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/Isar/rule_cases.ML	Sat Feb 11 17:17:45 2006 +0100
     1.2 +++ b/src/Pure/Isar/rule_cases.ML	Sat Feb 11 17:17:47 2006 +0100
     1.3 @@ -81,12 +81,12 @@
     1.4  
     1.5  fun extract_fixes NONE prop = (strip_params prop, [])
     1.6    | extract_fixes (SOME outline) prop =
     1.7 -      splitAt (length (Logic.strip_params outline), strip_params prop);
     1.8 +      chop (length (Logic.strip_params outline)) (strip_params prop);
     1.9  
    1.10  fun extract_assumes _ NONE prop = ([("", Logic.strip_assums_hyp prop)], [])
    1.11    | extract_assumes qual (SOME outline) prop =
    1.12        let val (hyps, prems) =
    1.13 -        splitAt (length (Logic.strip_assums_hyp outline), Logic.strip_assums_hyp prop)
    1.14 +        chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
    1.15        in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end;
    1.16  
    1.17  fun extract_case is_open thy (case_outline, raw_prop) name concls =
     2.1 --- a/src/Pure/Syntax/syn_ext.ML	Sat Feb 11 17:17:45 2006 +0100
     2.2 +++ b/src/Pure/Syntax/syn_ext.ML	Sat Feb 11 17:17:47 2006 +0100
     2.3 @@ -298,7 +298,7 @@
     2.4              err_in_mfix "Missing structure argument for indexed syntax" mfix;
     2.5  
     2.6            val xs = map Ast.Variable (Term.invent_names [] "xa" (length args - 1));
     2.7 -          val (xs1, xs2) = Library.splitAt (Library.find_index is_index args, xs);
     2.8 +          val (xs1, xs2) = chop (find_index is_index args) xs;
     2.9            val i = Ast.Variable "i";
    2.10            val lhs = Ast.mk_appl (Ast.Constant indexed_const)
    2.11              (xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2);
     3.1 --- a/src/Pure/Thy/thm_database.ML	Sat Feb 11 17:17:45 2006 +0100
     3.2 +++ b/src/Pure/Thy/thm_database.ML	Sat Feb 11 17:17:47 2006 +0100
     3.3 @@ -92,7 +92,7 @@
     3.4            else NONE;
     3.5          val names = NameSpace.unpack name;
     3.6        in
     3.7 -        (case #2 (splitAt (length names - 2, names)) of
     3.8 +        (case #2 (chop (length names - 2) names) of
     3.9            [bname] => result "" bname
    3.10          | [prfx, bname] => result (if prfx = thy_name then "" else prfx) bname
    3.11          | _ => NONE)
     4.1 --- a/src/Pure/proofterm.ML	Sat Feb 11 17:17:45 2006 +0100
     4.2 +++ b/src/Pure/proofterm.ML	Sat Feb 11 17:17:47 2006 +0100
     4.3 @@ -913,7 +913,7 @@
     4.4              val prop = (case prf of PThm (_, _, prop, _) => prop | PAxm (_, prop, _) => prop
     4.5                | Oracle (_, prop, _) => prop | _ => error "shrink: proof not in normal form");
     4.6              val vs = vars_of prop;
     4.7 -            val (ts', ts'') = splitAt (length vs, ts)
     4.8 +            val (ts', ts'') = chop (length vs) ts;
     4.9              val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts';
    4.10              val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
    4.11                insert (op =) ixn (case AList.lookup (op =) insts ixn of
     5.1 --- a/src/Pure/thm.ML	Sat Feb 11 17:17:45 2006 +0100
     5.2 +++ b/src/Pure/thm.ML	Sat Feb 11 17:17:47 2006 +0100
     5.3 @@ -1219,7 +1219,7 @@
     5.4      val Bi' =
     5.5        if 0 = m orelse m = n then Bi
     5.6        else if 0 < m andalso m < n then
     5.7 -        let val (ps, qs) = splitAt (m, asms)
     5.8 +        let val (ps, qs) = chop m asms
     5.9          in list_all (params, Logic.list_implies (qs @ ps, concl)) end
    5.10        else raise THM ("rotate_rule", k, [state]);
    5.11    in
    5.12 @@ -1249,7 +1249,7 @@
    5.13      val prop' =
    5.14        if 0 = m orelse m = n_j then prop
    5.15        else if 0 < m andalso m < n_j then
    5.16 -        let val (ps, qs) = splitAt (m, moved_prems)
    5.17 +        let val (ps, qs) = chop m moved_prems
    5.18          in Logic.list_implies (fixed_prems @ qs @ ps, concl) end
    5.19        else raise THM ("permute_prems: k", k, [rl]);
    5.20    in
     6.1 --- a/src/Pure/type_infer.ML	Sat Feb 11 17:17:45 2006 +0100
     6.2 +++ b/src/Pure/type_infer.ML	Sat Feb 11 17:17:47 2006 +0100
     6.3 @@ -342,7 +342,7 @@
     6.4      fun prep_output bs ts Ts =
     6.5        let
     6.6          val (Ts_bTs', ts') = typs_terms_of [] PTFree "??" (Ts @ map snd bs, ts);
     6.7 -        val (Ts',Ts'') = Library.splitAt(length Ts, Ts_bTs');
     6.8 +        val (Ts', Ts'') = chop (length Ts) Ts_bTs';
     6.9          val xs = map Free (map fst bs ~~ Ts'');
    6.10          val ts'' = map (fn t => subst_bounds (xs, t)) ts';
    6.11        in (ts'', Ts') end;