--- a/src/FOLP/simp.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/FOLP/simp.ML Thu Oct 22 13:48:06 2009 +0200
@@ -534,7 +534,7 @@
fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) =
let fun xn_list(x,n) =
- let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n);
+ let val ixs = map_range (fn i => (x^(radixstring(26,"a",i)),0)) (n - 1);
in ListPair.map eta_Var (ixs, Library.take(n+1,Ts)) end
val lhs = list_comb(f,xn_list("X",k-1))
val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik)
--- a/src/HOL/Decision_Procs/Cooper.thy Thu Oct 22 10:52:07 2009 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Thu Oct 22 13:48:06 2009 +0200
@@ -2035,8 +2035,8 @@
val t = Thm.term_of ct;
val fs = OldTerm.term_frees t;
val bs = term_bools [] t;
- val vs = fs ~~ (0 upto (length fs - 1))
- val ps = bs ~~ (0 upto (length bs - 1))
+ val vs = map_index swap fs;
+ val ps = map_index swap bs;
val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t;
in (Thm.cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
end;
--- a/src/HOL/Decision_Procs/Ferrack.thy Thu Oct 22 10:52:07 2009 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Thu Oct 22 13:48:06 2009 +0200
@@ -2073,7 +2073,7 @@
val thy = Thm.theory_of_cterm ct;
val t = Thm.term_of ct;
val fs = OldTerm.term_frees t;
- val vs = fs ~~ (0 upto (length fs - 1));
+ val vs = map_index swap fs;
val res = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (@{code linrqe} (fm_of_term vs t))));
in Thm.cterm_of thy res end
end;
--- a/src/HOL/Decision_Procs/MIR.thy Thu Oct 22 10:52:07 2009 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Thu Oct 22 13:48:06 2009 +0200
@@ -5898,7 +5898,7 @@
val thy = Thm.theory_of_cterm ct;
val t = Thm.term_of ct;
val fs = OldTerm.term_frees t;
- val vs = fs ~~ (0 upto (length fs - 1));
+ val vs = map_index swap fs;
val qe = if proofs then @{code mirlfrqe} else @{code mircfrqe};
val t' = (term_of_fm vs o qe o fm_of_term vs) t;
in (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Thu Oct 22 13:48:06 2009 +0200
@@ -965,8 +965,8 @@
else if d = 0 then [FuncUtil.Ctermfunc.empty]
else if null vars then [monomial_1] else
let val alts =
- map (fn k => let val oths = enumerate_monomials (d - k) (tl vars)
- in map (fn ks => if k = 0 then ks else FuncUtil.Ctermfunc.update (hd vars, k) ks) oths end) (0 upto d)
+ map_range (fn k => let val oths = enumerate_monomials (d - k) (tl vars)
+ in map (fn ks => if k = 0 then ks else FuncUtil.Ctermfunc.update (hd vars, k) ks) oths end) (d + 1)
in flat alts
end;
@@ -1202,9 +1202,9 @@
val eq0 = map (poly_of_term o Thm.dest_arg1 o concl) eqs
val le0 = map (poly_of_term o Thm.dest_arg o concl) les
val lt0 = map (poly_of_term o Thm.dest_arg o concl) lts
- val eqp0 = map (fn (t,i) => (t,RealArith.Axiom_eq i)) (eq0 ~~ (0 upto (length eq0 - 1)))
- val lep0 = map (fn (t,i) => (t,RealArith.Axiom_le i)) (le0 ~~ (0 upto (length le0 - 1)))
- val ltp0 = map (fn (t,i) => (t,RealArith.Axiom_lt i)) (lt0 ~~ (0 upto (length lt0 - 1)))
+ val eqp0 = map_index (fn (i, t) => (t,RealArith.Axiom_eq i)) eq0
+ val lep0 = map_index (fn (i, t) => (t,RealArith.Axiom_le i)) le0
+ val ltp0 = map_index (fn (i, t) => (t,RealArith.Axiom_lt i)) lt0
val (keq,eq) = List.partition (fn (p,_) => multidegree p = 0) eqp0
val (klep,lep) = List.partition (fn (p,_) => multidegree p = 0) lep0
val (kltp,ltp) = List.partition (fn (p,_) => multidegree p = 0) ltp0
--- a/src/HOL/Library/positivstellensatz.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Thu Oct 22 13:48:06 2009 +0200
@@ -643,9 +643,9 @@
fun linear_prover (eq,le,lt) =
let
- val eqs = map2 (fn p => fn n => (p,Axiom_eq n)) eq (0 upto (length eq - 1))
- val les = map2 (fn p => fn n => (p,Axiom_le n)) le (0 upto (length le - 1))
- val lts = map2 (fn p => fn n => (p,Axiom_lt n)) lt (0 upto (length lt - 1))
+ val eqs = map_index (fn (n, p) => (p,Axiom_eq n)) eq
+ val les = map_index (fn (n, p) => (p,Axiom_le n)) le
+ val lts = map_index (fn (n, p) => (p,Axiom_lt n)) lt
in linear_eqs(eqs,les,lts)
end
--- a/src/HOL/Nominal/nominal_datatype.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Thu Oct 22 13:48:06 2009 +0200
@@ -102,7 +102,7 @@
(**** make datatype info ****)
fun make_dt_info descr sorts induct reccomb_names rec_thms
- (((i, (_, (tname, _, _))), distinct), inject) =
+ (i, (((_, (tname, _, _)), distinct), inject)) =
(tname,
{index = i,
descr = descr,
@@ -2045,8 +2045,8 @@
end) (rec_eq_prems ~~
DatatypeProp.make_primrecs new_type_names descr' sorts thy12);
- val dt_infos = map (make_dt_info pdescr sorts induct reccomb_names rec_thms)
- ((0 upto length descr1 - 1) ~~ descr1 ~~ distinct_thms ~~ inject_thms);
+ val dt_infos = map_index (make_dt_info pdescr sorts induct reccomb_names rec_thms)
+ (descr1 ~~ distinct_thms ~~ inject_thms);
(* FIXME: theorems are stored in database for testing only *)
val (_, thy13) = thy12 |>
--- a/src/HOL/SizeChange/sct.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/HOL/SizeChange/sct.ML Thu Oct 22 13:48:06 2009 +0200
@@ -156,9 +156,9 @@
val mk_number = HOLogic.mk_nat
val dest_number = HOLogic.dest_nat
-fun nums_to i = map mk_number (0 upto (i - 1))
+fun nums_to i = map_range mk_number i
-val nth_simps = [thm "List.nth_Cons_0", thm "List.nth_Cons_Suc"]
+val nth_simps = [@{thm List.nth_Cons_0}, @{thm List.nth_Cons_Suc}]
val nth_ss = (HOL_basic_ss addsimps nth_simps)
val simp_nth_tac = simp_tac nth_ss
@@ -166,7 +166,7 @@
fun tabulate_tlist thy l =
let
val n = length (HOLogic.dest_list l)
- val table = Inttab.make (map (fn i => (i, Simplifier.rewrite nth_ss (cterm_of thy (mk_nth l $ mk_number i)))) (0 upto n - 1))
+ val table = Inttab.make (map_range (fn i => (i, Simplifier.rewrite nth_ss (cterm_of thy (mk_nth l $ mk_number i)))) n)
in
the o Inttab.lookup table
end
@@ -250,7 +250,7 @@
val goal = HOLogic.mk_Trueprop (mk_approx (Var (("G", 0), scgT)) RD1 RD2 Ms1 Ms2)
- val tac = (EVERY (map (fn n => EVERY (map (set_m1 n) (0 upto M - 1))) (0 upto N - 1)))
+ val tac = (EVERY (map_range (fn n => EVERY (map_range (set_m1 n) M)) N))
THEN (rtac approx_empty 1)
val approx_thm = goal
--- a/src/HOL/String.thy Thu Oct 22 10:52:07 2009 +0200
+++ b/src/HOL/String.thy Thu Oct 22 13:48:06 2009 +0200
@@ -48,7 +48,7 @@
setup {*
let
- val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15);
+ val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
val thms = map_product
(fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
nibbles nibbles;
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Oct 22 13:48:06 2009 +0200
@@ -56,7 +56,7 @@
val {maxidx, ...} = rep_thm induct;
val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
- fun prove_casedist_thm ((i, t), T) =
+ fun prove_casedist_thm (i, (T, t)) =
let
val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) =>
Abs ("z", T', Const ("True", T''))) induct_Ps;
@@ -77,8 +77,8 @@
REPEAT (rtac TrueI 1)])
end;
- val casedist_thms = map prove_casedist_thm ((0 upto (length newTs - 1)) ~~
- (DatatypeProp.make_casedists descr sorts) ~~ newTs)
+ val casedist_thms = map_index prove_casedist_thm
+ (newTs ~~ DatatypeProp.make_casedists descr sorts)
in
thy
|> store_thms_atts "exhaust" new_type_names (map single case_names_exhausts) casedist_thms
--- a/src/HOL/Tools/Function/induction_scheme.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/HOL/Tools/Function/induction_scheme.ML Thu Oct 22 13:48:06 2009 +0200
@@ -363,7 +363,7 @@
val ineqss = mk_ineqs R scheme
|> map (map (pairself (assume o cert)))
- val complete = map (mk_completeness ctxt scheme #> cert #> assume) (0 upto (length branches - 1))
+ val complete = map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
val wf_thm = mk_wf ctxt R scheme |> cert |> assume
val (descent, pres) = split_list (flat ineqss)
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Oct 22 13:48:06 2009 +0200
@@ -119,7 +119,7 @@
G (p, q, edges)
end
in
- GP (map arity (0 upto n - 1), map mk_graph cs)
+ GP (map_range arity n, map mk_graph cs)
end
(* General reduction pair application *)
@@ -312,8 +312,8 @@
fun print_error ctxt D = CALLS (fn (cs, i) =>
let
val np = get_num_points D
- val ms = map (get_measures D) (0 upto np - 1)
- val tys = map (get_types D) (0 upto np - 1)
+ val ms = map_range (get_measures D) np
+ val tys = map_range (get_types D) np
fun index xs = (1 upto length xs) ~~ xs
fun outp s t f xs = map (fn (x, y) => s ^ Int.toString x ^ t ^ f y ^ "\n") xs
val ims = index (map index ms)
--- a/src/HOL/Tools/Function/scnp_solve.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_solve.ML Thu Oct 22 13:48:06 2009 +0200
@@ -63,8 +63,8 @@
/ \ f i
0<=i<n
*)
-fun iforall n f = all (map f (0 upto n - 1))
-fun iexists n f = PropLogic.exists (map f (0 upto n - 1))
+fun iforall n f = all (map_range f n)
+fun iexists n f = PropLogic.exists (map_range f n)
fun iforall2 n m f = all (map_product f (0 upto n - 1) (0 upto m - 1))
fun the_one var n x = all (var x :: map (Not o var) (remove (op =) x (0 upto n - 1)))
@@ -221,7 +221,7 @@
let fun prog_pt_mapping p =
map_filter (fn x => if assign (P(p, x)) then SOME (x, assignTag p x) else NONE)
(0 upto (arity gp p) - 1)
- in map prog_pt_mapping (0 upto num_prog_pts gp - 1) end
+ in map_range prog_pt_mapping (num_prog_pts gp) end
val strict_list = filter (assign o STRICT) (0 upto num_graphs gp - 1)
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Thu Oct 22 13:48:06 2009 +0200
@@ -312,7 +312,7 @@
(* Overall function. *)
fun grobner pols =
- let val npols = map2 (fn p => fn n => (p,Start n)) pols (0 upto (length pols - 1))
+ let val npols = map_index (fn (n, p) => (p, Start n)) pols
val phists = filter (fn (p,_) => not (null p)) npols
val bas = grobner_interreduce [] (map monic phists)
val prs0 = map_product pair bas bas
@@ -802,8 +802,8 @@
val pols = map (grobify_term vars) tms
val pol = grobify_term vars tm
val cert = grobner_ideal vars pols pol
- in map (fn n => these (AList.lookup (op =) cert n) |> holify_polynomial vars)
- (0 upto (length pols - 1))
+ in map_range (fn n => these (AList.lookup (op =) cert n) |> holify_polynomial vars)
+ (length pols)
end
fun poly_eq_conv t =
--- a/src/HOL/Tools/TFL/tfl.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Thu Oct 22 13:48:06 2009 +0200
@@ -54,8 +54,6 @@
val list_mk_type = U.end_itlist (curry (op -->));
-fun enumerate xs = ListPair.zip(xs, 0 upto (length xs - 1));
-
fun front_last [] = raise TFL_ERR "front_last" "empty list"
| front_last [x] = ([],x)
| front_last (h::t) =
@@ -328,7 +326,7 @@
val (fname,ftype) = dest_atom atom
val dummy = map (no_repeat_vars thy) pats
val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
- map (fn (t,i) => (t,(i,true))) (enumerate R))
+ map_index (fn (i, t) => (t,(i,true))) R)
val names = List.foldr OldTerm.add_term_names [] R
val atype = type_of(hd pats)
and aname = Name.variant names "a"
--- a/src/HOL/Tools/inductive_codegen.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Thu Oct 22 13:48:06 2009 +0200
@@ -625,7 +625,7 @@
fun conv_ntuple fs ts p =
let
val k = length fs;
- val xs = map (fn i => str ("x" ^ string_of_int i)) (0 upto k);
+ val xs = map_range (fn i => str ("x" ^ string_of_int i)) (k + 1);
val xs' = map (fn Bound i => nth xs (k - i)) ts;
fun conv xs js =
if js mem fs then
--- a/src/HOL/Tools/record.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/HOL/Tools/record.ML Thu Oct 22 13:48:06 2009 +0200
@@ -1894,8 +1894,8 @@
more;
in
if more = HOLogic.unit
- then build (map recT (0 upto parent_len))
- else build (map rec_schemeT (0 upto parent_len))
+ then build (map_range recT (parent_len + 1))
+ else build (map_range rec_schemeT (parent_len + 1))
end;
val r_rec0 = mk_rec all_vars_more 0;
--- a/src/HOL/Tools/refute.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/HOL/Tools/refute.ML Thu Oct 22 13:48:06 2009 +0200
@@ -2618,8 +2618,7 @@
"unexpected size of IDT (wrong type associated?)")
else ()
(* interpretation *)
- val rec_op = Node (map (compute_array_entry idt_index)
- (0 upto (idt_size - 1)))
+ val rec_op = Node (map_range (compute_array_entry idt_index) idt_size)
in
SOME (rec_op, model', args')
end
@@ -2784,8 +2783,8 @@
(replicate (size_of_nat - element - 1) False))
end
in
- SOME (Node (map (fn m => Node (map (plus m) (0 upto size_of_nat-1)))
- (0 upto size_of_nat-1)), model, args)
+ SOME (Node (map_range (fn m => Node (map_range (plus m) size_of_nat)) size_of_nat),
+ model, args)
end
| _ =>
NONE;
@@ -2812,8 +2811,8 @@
(replicate (size_of_nat - element - 1) False))
end
in
- SOME (Node (map (fn m => Node (map (minus m) (0 upto size_of_nat-1)))
- (0 upto size_of_nat-1)), model, args)
+ SOME (Node (map_range (fn m => Node (map_range (minus m) size_of_nat)) size_of_nat),
+ model, args)
end
| _ =>
NONE;
@@ -2843,8 +2842,8 @@
(replicate (size_of_nat - element - 1) False))
end
in
- SOME (Node (map (fn m => Node (map (mult m) (0 upto size_of_nat-1)))
- (0 upto size_of_nat-1)), model, args)
+ SOME (Node (map_range (fn m => Node (map_range (mult m) size_of_nat)) size_of_nat),
+ model, args)
end
| _ =>
NONE;
--- a/src/Provers/order.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/Provers/order.ML Thu Oct 22 13:48:06 2009 +0200
@@ -731,9 +731,6 @@
in u :: dfs_visit g u end;
-fun indexComps components =
- ListPair.map (fn (a,b) => (a,b)) (0 upto (length components -1), components);
-
fun indexNodes IndexComp =
maps (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp;
@@ -1109,7 +1106,7 @@
| mk_sccGraphs components leqG neqG ntc =
let
(* Liste (Index der Komponente, Komponente *)
- val IndexComp = indexComps components;
+ val IndexComp = map_index I components;
fun handleContr edge g =
@@ -1211,7 +1208,7 @@
let
val (leqG, neqG, neqE) = mkGraphs asms
val components = scc_term leqG
- val ntc = indexNodes (indexComps components)
+ val ntc = indexNodes (map_index I components)
val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc
in
let
--- a/src/Provers/quasi.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/Provers/quasi.ML Thu Oct 22 13:48:06 2009 +0200
@@ -118,8 +118,8 @@
(* *)
(* ************************************************************************ *)
-fun mkasm_trans sign (t, n) =
- case Less.decomp_trans sign t of
+fun mkasm_trans thy (t, n) =
+ case Less.decomp_trans thy t of
SOME (x, rel, y) =>
(case rel of
"<=" => [Le (x, y, Asm n)]
@@ -137,8 +137,8 @@
(* *)
(* ************************************************************************ *)
-fun mkasm_quasi sign (t, n) =
- case Less.decomp_quasi sign t of
+fun mkasm_quasi thy (t, n) =
+ case Less.decomp_quasi thy t of
SOME (x, rel, y) => (case rel of
"<" => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE))
else [Less (x, y, Asm n)]
@@ -164,8 +164,8 @@
(* ************************************************************************ *)
-fun mkconcl_trans sign t =
- case Less.decomp_trans sign t of
+fun mkconcl_trans thy t =
+ case Less.decomp_trans thy t of
SOME (x, rel, y) => (case rel of
"<=" => (Le (x, y, Asm ~1), Asm 0)
| _ => raise Cannot)
@@ -181,8 +181,8 @@
(* *)
(* ************************************************************************ *)
-fun mkconcl_quasi sign t =
- case Less.decomp_quasi sign t of
+fun mkconcl_quasi thy t =
+ case Less.decomp_quasi thy t of
SOME (x, rel, y) => (case rel of
"<" => ([Less (x, y, Asm ~1)], Asm 0)
| "<=" => ([Le (x, y, Asm ~1)], Asm 0)
@@ -503,12 +503,12 @@
(* *)
(* *********************************************************************** *)
-fun solveLeTrans sign (asms, concl) =
+fun solveLeTrans thy (asms, concl) =
let
val g = mkGraph asms
in
let
- val (subgoal, prf) = mkconcl_trans sign concl
+ val (subgoal, prf) = mkconcl_trans thy concl
val (found, path) = findPath (lower subgoal) (upper subgoal) g
in
if found then [getprf (transPath (tl path, hd path))]
@@ -526,12 +526,12 @@
(* *)
(* *********************************************************************** *)
-fun solveQuasiOrder sign (asms, concl) =
+fun solveQuasiOrder thy (asms, concl) =
let
val (leG, neqE) = mkQuasiGraph asms
in
let
- val (subgoals, prf) = mkconcl_quasi sign concl
+ val (subgoals, prf) = mkconcl_quasi thy concl
fun solve facts less =
(case triv_solv less of NONE => findQuasiProof (leG, neqE) less
| SOME prf => prf )
@@ -555,7 +555,7 @@
val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
- val lesss = flat (ListPair.map (mkasm_trans thy) (Hs, 0 upto (length Hs - 1)));
+ val lesss = flat (map_index (mkasm_trans thy o swap) Hs);
val prfs = solveLeTrans thy (lesss, C);
val (subgoal, prf) = mkconcl_trans thy C;
@@ -576,7 +576,7 @@
val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
- val lesss = flat (ListPair.map (mkasm_quasi thy) (Hs, 0 upto (length Hs - 1)));
+ val lesss = flat (map_index (mkasm_quasi thy o swap) Hs);
val prfs = solveQuasiOrder thy (lesss, C);
val (subgoals, prf) = mkconcl_quasi thy C;
in
--- a/src/Provers/trancl.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/Provers/trancl.ML Thu Oct 22 13:48:06 2009 +0200
@@ -538,7 +538,7 @@
val C = Logic.strip_assums_concl A;
val (rel, subgoals, prf) = mkconcl_trancl C;
- val prems = flat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)));
+ val prems = flat (map_index (mkasm_trancl rel o swap) Hs);
val prfs = solveTrancl (prems, C);
in
Subgoal.FOCUS (fn {prems, ...} =>
@@ -555,7 +555,7 @@
val C = Logic.strip_assums_concl A;
val (rel, subgoals, prf) = mkconcl_rtrancl C;
- val prems = flat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)));
+ val prems = flat (map_index (mkasm_rtrancl rel o swap) Hs);
val prfs = solveRtrancl (prems, C);
in
Subgoal.FOCUS (fn {prems, ...} =>
--- a/src/Pure/Syntax/parser.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/Pure/Syntax/parser.ML Thu Oct 22 13:48:06 2009 +0200
@@ -840,7 +840,7 @@
fun guess_infix_lr (Gram gram) c = (*based on educated guess*)
let
- fun freeze a = map (curry Array.sub a) (0 upto Array.length a - 1);
+ fun freeze a = map_range (curry Array.sub a) (Array.length a);
val prods = maps snd (maps snd (freeze (#prods gram)));
fun guess (SOME ([Nonterminal (_, k), Terminal (Token (Literal, s, _)), Nonterminal (_, l)], _, j)) =
if k = j andalso l = j + 1 then SOME (s, true, false, j)
--- a/src/Pure/library.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/Pure/library.ML Thu Oct 22 13:48:06 2009 +0200
@@ -89,6 +89,7 @@
val nth_list: 'a list list -> int -> 'a list
val map_index: (int * 'a -> 'b) -> 'a list -> 'b list
val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
+ val map_range: (int -> 'a) -> int -> 'a list
val split_last: 'a list -> 'a list * 'a
val find_index: ('a -> bool) -> 'a list -> int
val find_first: ('a -> bool) -> 'a list -> 'a option
@@ -463,6 +464,12 @@
| fold_aux i (x :: xs) y = fold_aux (i + 1) xs (f (i, x) y);
in fold_aux 0 end;
+fun map_range f i =
+ let
+ fun mapp k =
+ if k < i then f k :: mapp (k + 1) else [];
+ in mapp 0 end;
+
val last_elem = List.last;
(*rear decomposition*)
--- a/src/Pure/term.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/Pure/term.ML Thu Oct 22 13:48:06 2009 +0200
@@ -939,7 +939,7 @@
| free_dummy_patterns a used = (a, used);
fun replace_dummy Ts (Const ("dummy_pattern", T)) i =
- (list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)), i + 1)
+ (list_comb (Var (("_dummy_", i), Ts ---> T), map_range Bound (length Ts)), i + 1)
| replace_dummy Ts (Abs (x, T, t)) i =
let val (t', i') = replace_dummy (T :: Ts) t i
in (Abs (x, T, t'), i') end
--- a/src/Pure/unify.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/Pure/unify.ML Thu Oct 22 13:48:06 2009 +0200
@@ -531,12 +531,12 @@
Bound vars in the binder are "banned" unless used in both t AND u *)
fun clean_ffpair thy ((rbinder, t, u), (env,tpairs)) =
let val loot = loose_bnos t and loou = loose_bnos u
- fun add_index (((a,T), j), (bnos, newbinder)) =
+ fun add_index (j, (a,T)) (bnos, newbinder) =
if member (op =) loot j andalso member (op =) loou j
then (bnos, (a,T)::newbinder) (*needed by both: keep*)
else (j::bnos, newbinder); (*remove*)
- val indices = 0 upto (length rbinder - 1);
- val (banned,rbin') = List.foldr add_index ([],[]) (rbinder~~indices);
+ val (banned,rbin') = fold_rev add_index
+ ((0 upto (length rbinder - 1)) ~~ rbinder) ([],[]);
val (env', t') = clean_term banned (env, t);
val (env'',u') = clean_term banned (env',u)
in (ff_assign thy (env'', rbin', t', u'), tpairs)
--- a/src/Tools/Code/code_preproc.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML Thu Oct 22 13:48:06 2009 +0200
@@ -408,9 +408,8 @@
in Thm.instantiate (insts, []) thm end;
fun add_arity thy vardeps (class, tyco) =
- AList.default (op =)
- ((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k))
- (0 upto Sign.arity_number thy tyco - 1));
+ AList.default (op =) ((class, tyco),
+ map_range (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k)) (Sign.arity_number thy tyco));
fun add_eqs thy vardeps (c, (proto_lhs, proto_eqns)) (rhss, eqngr) =
if can (Graph.get_node eqngr) c then (rhss, eqngr)