1.1 --- a/NEWS Fri Nov 26 23:12:01 2010 +0100
1.2 +++ b/NEWS Fri Nov 26 23:41:23 2010 +0100
1.3 @@ -521,6 +521,9 @@
1.4
1.5 *** ML ***
1.6
1.7 +* Former exception Library.UnequalLengths now coincides with
1.8 +ListPair.UnequalLengths.
1.9 +
1.10 * Renamed raw "explode" function to "raw_explode" to emphasize its
1.11 meaning. Note that internally to Isabelle, Symbol.explode is used in
1.12 almost all situations.
2.1 --- a/src/HOL/Fun.thy Fri Nov 26 23:12:01 2010 +0100
2.2 +++ b/src/HOL/Fun.thy Fri Nov 26 23:41:23 2010 +0100
2.3 @@ -155,11 +155,6 @@
2.4 shows "inj f"
2.5 using assms unfolding inj_on_def by auto
2.6
2.7 -text{*For Proofs in @{text "Tools/Datatype/datatype_rep_proofs"}*}
2.8 -lemma datatype_injI:
2.9 - "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)"
2.10 -by (simp add: inj_on_def)
2.11 -
2.12 theorem range_ex1_eq: "inj f \<Longrightarrow> b : range f = (EX! x. b = f x)"
2.13 by (unfold inj_on_def, blast)
2.14
3.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Nov 26 23:12:01 2010 +0100
3.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Nov 26 23:41:23 2010 +0100
3.3 @@ -103,11 +103,6 @@
3.4
3.5 fun iszero (k,r) = r =/ rat_0;
3.6
3.7 -fun fold_rev2 f l1 l2 b =
3.8 - case (l1,l2) of
3.9 - ([],[]) => b
3.10 - | (h1::t1,h2::t2) => f h1 h2 (fold_rev2 f t1 t2 b)
3.11 - | _ => error "fold_rev2";
3.12
3.13 (* Vectors. Conventionally indexed 1..n. *)
3.14
4.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Nov 26 23:12:01 2010 +0100
4.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Nov 26 23:41:23 2010 +0100
4.3 @@ -19,7 +19,7 @@
4.4 lemma injective_scaleR:
4.5 assumes "(c :: real) ~= 0"
4.6 shows "inj (%(x :: 'n::euclidean_space). scaleR c x)"
4.7 -by (metis assms datatype_injI injI real_vector.scale_cancel_left)
4.8 + by (metis assms injI real_vector.scale_cancel_left)
4.9
4.10 lemma linear_add_cmul:
4.11 fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
5.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML Fri Nov 26 23:12:01 2010 +0100
5.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML Fri Nov 26 23:41:23 2010 +0100
5.3 @@ -117,13 +117,6 @@
5.4 [] => []
5.5 | h::t => map (cons h) (combinations (k - 1) t) @ combinations k t
5.6
5.7 -
5.8 -fun forall2 p l1 l2 = case (l1,l2) of
5.9 - ([],[]) => true
5.10 - | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2
5.11 - | _ => false;
5.12 -
5.13 -
5.14 fun vertices vs eqs =
5.15 let
5.16 fun vertex cmb = case solve(vs,cmb) of
5.17 @@ -131,16 +124,16 @@
5.18 | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v Rat.zero) vs)
5.19 val rawvs = map_filter vertex (combinations (length vs) eqs)
5.20 val unset = filter (forall (fn c => c >=/ Rat.zero)) rawvs
5.21 - in fold_rev (insert (uncurry (forall2 (curry op =/)))) unset []
5.22 + in fold_rev (insert (eq_list op =/)) unset []
5.23 end
5.24
5.25 -fun subsumes l m = forall2 (fn x => fn y => Rat.abs x <=/ Rat.abs y) l m
5.26 +val subsumes = eq_list (fn (x, y) => Rat.abs x <=/ Rat.abs y)
5.27
5.28 fun subsume todo dun = case todo of
5.29 [] => dun
5.30 |v::ovs =>
5.31 - let val dun' = if exists (fn w => subsumes w v) dun then dun
5.32 - else v::(filter (fn w => not(subsumes v w)) dun)
5.33 + let val dun' = if exists (fn w => subsumes (w, v)) dun then dun
5.34 + else v:: filter (fn w => not (subsumes (v, w))) dun
5.35 in subsume ovs dun'
5.36 end;
5.37
5.38 @@ -246,10 +239,6 @@
5.39 Const(@{const_name norm},_)$_ => arg_conv vector_canon_conv ct
5.40 | _ => raise CTERM ("norm_canon_conv", [ct])
5.41
5.42 -fun fold_rev2 f [] [] z = z
5.43 - | fold_rev2 f (x::xs) (y::ys) z = f x y (fold_rev2 f xs ys z)
5.44 - | fold_rev2 f _ _ _ = raise UnequalLengths;
5.45 -
5.46 fun int_flip v eq =
5.47 if FuncUtil.Intfunc.defined eq v
5.48 then FuncUtil.Intfunc.update (v, Rat.neg (FuncUtil.Intfunc.apply eq v)) eq else eq;
6.1 --- a/src/HOL/Tools/Datatype/datatype.ML Fri Nov 26 23:12:01 2010 +0100
6.2 +++ b/src/HOL/Tools/Datatype/datatype.ML Fri Nov 26 23:41:23 2010 +0100
6.3 @@ -54,6 +54,8 @@
6.4 val Suml_inject = @{thm Suml_inject};
6.5 val Sumr_inject = @{thm Sumr_inject};
6.6
6.7 +val datatype_injI =
6.8 + @{lemma "(!!x. ALL y. f x = f y --> x = y) ==> inj f" by (simp add: inj_on_def)};
6.9
6.10
6.11 (** proof of characteristic theorems **)
6.12 @@ -438,8 +440,7 @@
6.13 Lim_inject :: inj_thms') @ fun_congs) 1),
6.14 atac 1]))])])])]);
6.15
6.16 - val inj_thms'' = map (fn r => r RS @{thm datatype_injI})
6.17 - (split_conj_thm inj_thm);
6.18 + val inj_thms'' = map (fn r => r RS datatype_injI) (split_conj_thm inj_thm);
6.19
6.20 val elem_thm =
6.21 Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
7.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML Fri Nov 26 23:12:01 2010 +0100
7.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Fri Nov 26 23:41:23 2010 +0100
7.3 @@ -324,7 +324,7 @@
7.4 \ nested recursion")
7.5 | (SOME {index, descr, ...}) =>
7.6 let val (_, vars, _) = (the o AList.lookup (op =) descr) index;
7.7 - val subst = ((map dest_DtTFree vars) ~~ dts) handle Library.UnequalLengths =>
7.8 + val subst = ((map dest_DtTFree vars) ~~ dts) handle ListPair.UnequalLengths =>
7.9 typ_error T ("Type constructor " ^ tname ^ " used with wrong\
7.10 \ number of arguments")
7.11 in (i + index, map (fn (j, (tn, args, cs)) => (i + j,
8.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML Fri Nov 26 23:12:01 2010 +0100
8.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML Fri Nov 26 23:41:23 2010 +0100
8.3 @@ -48,8 +48,8 @@
8.4
8.5 fun make_tnames Ts =
8.6 let
8.7 - fun type_name (TFree (name, _)) = implode (tl (raw_explode name)) (* FIXME Symbol.explode (?) *)
8.8 - | type_name (Type (name, _)) =
8.9 + fun type_name (TFree (name, _)) = unprefix "'" name
8.10 + | type_name (Type (name, _)) =
8.11 let val name' = Long_Name.base_name name
8.12 in if Syntax.is_identifier name' then name' else "x" end;
8.13 in indexify_names (map type_name Ts) end;
9.1 --- a/src/HOL/Tools/Function/function_lib.ML Fri Nov 26 23:12:01 2010 +0100
9.2 +++ b/src/HOL/Tools/Function/function_lib.ML Fri Nov 26 23:41:23 2010 +0100
9.3 @@ -44,11 +44,11 @@
9.4
9.5 fun map4 _ [] [] [] [] = []
9.6 | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
9.7 - | map4 _ _ _ _ _ = raise Library.UnequalLengths;
9.8 + | map4 _ _ _ _ _ = raise ListPair.UnequalLengths;
9.9
9.10 fun map7 _ [] [] [] [] [] [] [] = []
9.11 | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) (b :: bs) = f x y z u v w b :: map7 f xs ys zs us vs ws bs
9.12 - | map7 _ _ _ _ _ _ _ _ = raise Library.UnequalLengths;
9.13 + | map7 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
9.14
9.15
9.16
10.1 --- a/src/HOL/Tools/Function/size.ML Fri Nov 26 23:12:01 2010 +0100
10.2 +++ b/src/HOL/Tools/Function/size.ML Fri Nov 26 23:41:23 2010 +0100
10.3 @@ -71,7 +71,7 @@
10.4 val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
10.5 map (fn T as TFree (s, _) =>
10.6 let
10.7 - val name = "f" ^ implode (tl (raw_explode s)); (* FIXME Symbol.explode (?) *)
10.8 + val name = "f" ^ unprefix "'" s;
10.9 val U = T --> HOLogic.natT
10.10 in
10.11 (((s, Free (name, U)), U), name)
11.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Nov 26 23:12:01 2010 +0100
11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Nov 26 23:41:23 2010 +0100
11.3 @@ -393,7 +393,7 @@
11.4 | do_mtype_comp cmp xs (M1 as MPair (M11, M12)) (M2 as MPair (M21, M22))
11.5 accum =
11.6 (accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)]
11.7 - handle Library.UnequalLengths =>
11.8 + handle ListPair.UnequalLengths =>
11.9 raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2], []))
11.10 | do_mtype_comp _ _ (MType _) (MType _) accum =
11.11 accum (* no need to compare them thanks to the cache *)
12.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Nov 26 23:12:01 2010 +0100
12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Nov 26 23:41:23 2010 +0100
12.3 @@ -527,7 +527,7 @@
12.4 | NONE =>
12.5 Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
12.6 $ Abs (s, T, kill ss Ts ts))
12.7 - | kill _ _ _ = raise UnequalLengths
12.8 + | kill _ _ _ = raise ListPair.UnequalLengths
12.9 fun gather ss Ts (Const (@{const_name Ex}, _) $ Abs (s1, T1, t1)) =
12.10 gather (ss @ [s1]) (Ts @ [T1]) t1
12.11 | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
13.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Nov 26 23:12:01 2010 +0100
13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Nov 26 23:41:23 2010 +0100
13.3 @@ -204,7 +204,7 @@
13.4
13.5 fun map3 _ [] [] [] = []
13.6 | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
13.7 - | map3 _ _ _ _ = raise UnequalLengths
13.8 + | map3 _ _ _ _ = raise ListPair.UnequalLengths
13.9
13.10 fun double_lookup eq ps key =
13.11 case AList.lookup (fn (SOME x, SOME y) => eq (x, y) | _ => false) ps
14.1 --- a/src/HOL/Tools/groebner.ML Fri Nov 26 23:12:01 2010 +0100
14.2 +++ b/src/HOL/Tools/groebner.ML Fri Nov 26 23:41:23 2010 +0100
14.3 @@ -233,14 +233,9 @@
14.4
14.5 fun align ((p,hp),(q,hq)) =
14.6 if poly_lt p q then ((p,hp),(q,hq)) else ((q,hq),(p,hp));
14.7 -fun forall2 p l1 l2 =
14.8 - case (l1,l2) of
14.9 - ([],[]) => true
14.10 - | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2
14.11 - | _ => false;
14.12
14.13 fun poly_eq p1 p2 =
14.14 - forall2 (fn (c1,m1) => fn (c2,m2) => c1 =/ c2 andalso (m1: int list) = m2) p1 p2;
14.15 + eq_list (fn ((c1, m1), (c2, m2)) => c1 =/ c2 andalso (m1: int list) = m2) (p1, p2);
14.16
14.17 fun memx ((p1,h1),(p2,h2)) ppairs =
14.18 not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs);
15.1 --- a/src/HOL/Tools/record.ML Fri Nov 26 23:12:01 2010 +0100
15.2 +++ b/src/HOL/Tools/record.ML Fri Nov 26 23:41:23 2010 +0100
15.3 @@ -917,7 +917,7 @@
15.4 val fields' = extern f :: map Long_Name.base_name fs;
15.5 val (args', more) = split_last args;
15.6 in (fields' ~~ args') @ strip_fields more end
15.7 - handle Library.UnequalLengths => [("", t)])
15.8 + handle ListPair.UnequalLengths => [("", t)])
15.9 | NONE => [("", t)])
15.10 | NONE => [("", t)])
15.11 | _ => [("", t)]);
16.1 --- a/src/HOL/Tools/refute.ML Fri Nov 26 23:12:01 2010 +0100
16.2 +++ b/src/HOL/Tools/refute.ML Fri Nov 26 23:41:23 2010 +0100
16.3 @@ -2953,9 +2953,7 @@
16.4 fun stlc_printer ctxt model T intr assignment =
16.5 let
16.6 (* string -> string *)
16.7 - fun strip_leading_quote s =
16.8 - (implode o (fn [] => [] | x::xs => if x="'" then xs else x::xs)
16.9 - o raw_explode) s (* FIXME Symbol.explode (?) *)
16.10 + val strip_leading_quote = perhaps (try (unprefix "'"))
16.11 (* Term.typ -> string *)
16.12 fun string_of_typ (Type (s, _)) = s
16.13 | string_of_typ (TFree (x, _)) = strip_leading_quote x
17.1 --- a/src/Pure/Proof/reconstruct.ML Fri Nov 26 23:12:01 2010 +0100
17.2 +++ b/src/Pure/Proof/reconstruct.ML Fri Nov 26 23:41:23 2010 +0100
17.3 @@ -137,7 +137,7 @@
17.4 NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env
17.5 | SOME Ts => (Ts, env));
17.6 val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
17.7 - (forall_intr_vfs prop) handle Library.UnequalLengths =>
17.8 + (forall_intr_vfs prop) handle ListPair.UnequalLengths =>
17.9 error ("Wrong number of type arguments for " ^ quote (Proofterm.guess_name prf))
17.10 in (prop', Proofterm.change_type (SOME Ts) prf, [], env', vTs) end;
17.11
18.1 --- a/src/Pure/consts.ML Fri Nov 26 23:12:01 2010 +0100
18.2 +++ b/src/Pure/consts.ML Fri Nov 26 23:41:23 2010 +0100
18.3 @@ -215,7 +215,7 @@
18.4 let
18.5 val declT = type_scheme consts c;
18.6 val vars = map Term.dest_TVar (typargs consts (c, declT));
18.7 - val inst = vars ~~ Ts handle UnequalLengths =>
18.8 + val inst = vars ~~ Ts handle ListPair.UnequalLengths =>
18.9 raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
18.10 in declT |> Term_Subst.instantiateT inst end;
18.11
19.1 --- a/src/Pure/drule.ML Fri Nov 26 23:12:01 2010 +0100
19.2 +++ b/src/Pure/drule.ML Fri Nov 26 23:41:23 2010 +0100
19.3 @@ -891,7 +891,7 @@
19.4 handle TYPE (msg, _, _) => err msg;
19.5
19.6 fun zip_vars xs ys =
19.7 - zip_options xs ys handle Library.UnequalLengths =>
19.8 + zip_options xs ys handle ListPair.UnequalLengths =>
19.9 err "more instantiations than variables in thm";
19.10
19.11 (*instantiate types first!*)
20.1 --- a/src/Pure/library.ML Fri Nov 26 23:12:01 2010 +0100
20.2 +++ b/src/Pure/library.ML Fri Nov 26 23:41:23 2010 +0100
20.3 @@ -58,7 +58,6 @@
20.4 val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
20.5
20.6 (*lists*)
20.7 - exception UnequalLengths
20.8 val single: 'a -> 'a list
20.9 val the_single: 'a list -> 'a
20.10 val singleton: ('a list -> 'b list) -> 'a -> 'b
20.11 @@ -97,6 +96,7 @@
20.12 val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
20.13 val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
20.14 val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
20.15 + val fold_rev2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
20.16 val forall2: ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
20.17 val zip_options: 'a list -> 'b option list -> ('a * 'b) list
20.18 val ~~ : 'a list * 'b list -> ('a * 'b) list
20.19 @@ -321,8 +321,6 @@
20.20
20.21 (** lists **)
20.22
20.23 -exception UnequalLengths;
20.24 -
20.25 fun single x = [x];
20.26
20.27 fun the_single [x] = x
20.28 @@ -495,7 +493,7 @@
20.29 let val (ps, qs) = chop (length xs) ys
20.30 in ps :: unflat xss qs end
20.31 | unflat [] [] = []
20.32 - | unflat _ _ = raise UnequalLengths;
20.33 + | unflat _ _ = raise ListPair.UnequalLengths;
20.34
20.35 fun burrow f xss = unflat xss (f (flat xss));
20.36
20.37 @@ -534,15 +532,17 @@
20.38
20.39 (* lists of pairs *)
20.40
20.41 -exception UnequalLengths;
20.42 -
20.43 fun map2 _ [] [] = []
20.44 | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys
20.45 - | map2 _ _ _ = raise UnequalLengths;
20.46 + | map2 _ _ _ = raise ListPair.UnequalLengths;
20.47
20.48 fun fold2 f [] [] z = z
20.49 | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z)
20.50 - | fold2 f _ _ _ = raise UnequalLengths;
20.51 + | fold2 f _ _ _ = raise ListPair.UnequalLengths;
20.52 +
20.53 +fun fold_rev2 f [] [] z = z
20.54 + | fold_rev2 f (x :: xs) (y :: ys) z = f x y (fold_rev2 f xs ys z)
20.55 + | fold_rev2 f _ _ _ = raise ListPair.UnequalLengths;
20.56
20.57 fun forall2 P [] [] = true
20.58 | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
20.59 @@ -558,13 +558,13 @@
20.60 fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys
20.61 | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys
20.62 | zip_options _ [] = []
20.63 - | zip_options [] _ = raise UnequalLengths;
20.64 + | zip_options [] _ = raise ListPair.UnequalLengths;
20.65
20.66 (*combine two lists forming a list of pairs:
20.67 [x1, ..., xn] ~~ [y1, ..., yn] ===> [(x1, y1), ..., (xn, yn)]*)
20.68 fun [] ~~ [] = []
20.69 | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys)
20.70 - | _ ~~ _ = raise UnequalLengths;
20.71 + | _ ~~ _ = raise ListPair.UnequalLengths;
20.72
20.73 (*inverse of ~~; the old 'split':
20.74 [(x1, y1), ..., (xn, yn)] ===> ([x1, ..., xn], [y1, ..., yn])*)
20.75 @@ -843,10 +843,11 @@
20.76
20.77 fun map_transpose f xss =
20.78 let
20.79 - val n = case distinct (op =) (map length xss)
20.80 - of [] => 0
20.81 + val n =
20.82 + (case distinct (op =) (map length xss) of
20.83 + [] => 0
20.84 | [n] => n
20.85 - | _ => raise UnequalLengths;
20.86 + | _ => raise ListPair.UnequalLengths);
20.87 in map_range (fn m => f (map (fn xs => nth xs m) xss)) n end;
20.88
20.89
20.90 @@ -1066,3 +1067,5 @@
20.91
20.92 structure Basic_Library: BASIC_LIBRARY = Library;
20.93 open Basic_Library;
20.94 +
20.95 +datatype legacy = UnequalLengths;
21.1 --- a/src/Pure/pattern.ML Fri Nov 26 23:12:01 2010 +0100
21.2 +++ b/src/Pure/pattern.ML Fri Nov 26 23:41:23 2010 +0100
21.3 @@ -365,7 +365,7 @@
21.4 and cases(binders,env as (iTs,itms),pat,obj) =
21.5 let val (ph,pargs) = strip_comb pat
21.6 fun rigrig1(iTs,oargs) = fold (mtch binders) (pargs~~oargs) (iTs,itms)
21.7 - handle UnequalLengths => raise MATCH
21.8 + handle ListPair.UnequalLengths => raise MATCH
21.9 fun rigrig2((a:string,Ta),(b,Tb),oargs) =
21.10 if a <> b then raise MATCH
21.11 else rigrig1(typ_match thy (Ta,Tb) iTs, oargs)
22.1 --- a/src/Tools/eqsubst.ML Fri Nov 26 23:12:01 2010 +0100
22.2 +++ b/src/Tools/eqsubst.ML Fri Nov 26 23:41:23 2010 +0100
22.3 @@ -235,13 +235,13 @@
22.4 val initenv =
22.5 Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
22.6 val useq = Unify.smash_unifiers thry [a] initenv
22.7 - handle UnequalLengths => Seq.empty
22.8 + handle ListPair.UnequalLengths => Seq.empty
22.9 | Term.TERM _ => Seq.empty;
22.10 fun clean_unify' useq () =
22.11 (case (Seq.pull useq) of
22.12 NONE => NONE
22.13 | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
22.14 - handle UnequalLengths => NONE
22.15 + handle ListPair.UnequalLengths => NONE
22.16 | Term.TERM _ => NONE
22.17 in
22.18 (Seq.make (clean_unify' useq))
23.1 --- a/src/Tools/induct_tacs.ML Fri Nov 26 23:12:01 2010 +0100
23.2 +++ b/src/Tools/induct_tacs.ML Fri Nov 26 23:41:23 2010 +0100
23.3 @@ -96,7 +96,7 @@
23.4 val _ = Method.trace ctxt [rule'];
23.5
23.6 val concls = Logic.dest_conjunctions (Thm.concl_of rule);
23.7 - val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
23.8 + val insts = maps prep_inst (concls ~~ varss) handle ListPair.UnequalLengths =>
23.9 error "Induction rule has different numbers of variables";
23.10 in res_inst_tac ctxt insts rule' i st end
23.11 handle THM _ => Seq.empty;