make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;

--- a/NEWS	Fri Nov 26 22:04:33 2010 +0100
+++ b/NEWS	Fri Nov 26 22:29:41 2010 +0100
@@ -507,6 +507,9 @@
 
 *** ML ***
 
+* Former exception Library.UnequalLengths now coincides with
+ListPair.UnequalLengths.
+
 * Renamed raw "explode" function to "raw_explode" to emphasize its
 meaning.  Note that internally to Isabelle, Symbol.explode is used in
 almost all situations.

--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Nov 26 22:04:33 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Nov 26 22:29:41 2010 +0100
@@ -324,7 +324,7 @@
            \ nested recursion")
        | (SOME {index, descr, ...}) =>
            let val (_, vars, _) = (the o AList.lookup (op =) descr) index;
-               val subst = ((map dest_DtTFree vars) ~~ dts) handle Library.UnequalLengths =>
+               val subst = ((map dest_DtTFree vars) ~~ dts) handle ListPair.UnequalLengths =>
                  typ_error T ("Type constructor " ^ tname ^ " used with wrong\
                   \ number of arguments")
            in (i + index, map (fn (j, (tn, args, cs)) => (i + j,

--- a/src/HOL/Tools/Function/function_lib.ML	Fri Nov 26 22:04:33 2010 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML	Fri Nov 26 22:29:41 2010 +0100
@@ -44,11 +44,11 @@
 
 fun map4 _ [] [] [] [] = []
   | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
-  | map4 _ _ _ _ _ = raise Library.UnequalLengths;
+  | map4 _ _ _ _ _ = raise ListPair.UnequalLengths;
 
 fun map7 _ [] [] [] [] [] [] [] = []
   | 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
-  | map7 _ _ _ _ _ _ _ _ = raise Library.UnequalLengths;
+  | map7 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
 
 
 

--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Nov 26 22:04:33 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Nov 26 22:29:41 2010 +0100
@@ -393,7 +393,7 @@
   | do_mtype_comp cmp xs (M1 as MPair (M11, M12)) (M2 as MPair (M21, M22))
                   accum =
     (accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)]
-     handle Library.UnequalLengths =>
+     handle ListPair.UnequalLengths =>
             raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2], []))
   | do_mtype_comp _ _ (MType _) (MType _) accum =
     accum (* no need to compare them thanks to the cache *)

--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Nov 26 22:04:33 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Nov 26 22:29:41 2010 +0100
@@ -527,7 +527,7 @@
          | NONE =>
            Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
            $ Abs (s, T, kill ss Ts ts))
-      | kill _ _ _ = raise UnequalLengths
+      | kill _ _ _ = raise ListPair.UnequalLengths
     fun gather ss Ts (Const (@{const_name Ex}, _) $ Abs (s1, T1, t1)) =
         gather (ss @ [s1]) (Ts @ [T1]) t1
       | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)

--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Nov 26 22:04:33 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Nov 26 22:29:41 2010 +0100
@@ -204,7 +204,7 @@
 
 fun map3 _ [] [] [] = []
   | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
-  | map3 _ _ _ _ = raise UnequalLengths
+  | map3 _ _ _ _ = raise ListPair.UnequalLengths
 
 fun double_lookup eq ps key =
   case AList.lookup (fn (SOME x, SOME y) => eq (x, y) | _ => false) ps

--- a/src/HOL/Tools/record.ML	Fri Nov 26 22:04:33 2010 +0100
+++ b/src/HOL/Tools/record.ML	Fri Nov 26 22:29:41 2010 +0100
@@ -917,7 +917,7 @@
                     val fields' = extern f :: map Long_Name.base_name fs;
                     val (args', more) = split_last args;
                   in (fields' ~~ args') @ strip_fields more end
-                  handle Library.UnequalLengths => [("", t)])
+                  handle ListPair.UnequalLengths => [("", t)])
               | NONE => [("", t)])
           | NONE => [("", t)])
        | _ => [("", t)]);

--- a/src/Pure/Proof/reconstruct.ML	Fri Nov 26 22:04:33 2010 +0100
+++ b/src/Pure/Proof/reconstruct.ML	Fri Nov 26 22:29:41 2010 +0100
@@ -137,7 +137,7 @@
                 NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env
               | SOME Ts => (Ts, env));
             val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
-              (forall_intr_vfs prop) handle Library.UnequalLengths =>
+              (forall_intr_vfs prop) handle ListPair.UnequalLengths =>
                 error ("Wrong number of type arguments for " ^ quote (Proofterm.guess_name prf))
           in (prop', Proofterm.change_type (SOME Ts) prf, [], env', vTs) end;
 

--- a/src/Pure/consts.ML	Fri Nov 26 22:04:33 2010 +0100
+++ b/src/Pure/consts.ML	Fri Nov 26 22:29:41 2010 +0100
@@ -215,7 +215,7 @@
   let
     val declT = type_scheme consts c;
     val vars = map Term.dest_TVar (typargs consts (c, declT));
-    val inst = vars ~~ Ts handle UnequalLengths =>
+    val inst = vars ~~ Ts handle ListPair.UnequalLengths =>
       raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
   in declT |> Term_Subst.instantiateT inst end;
 

--- a/src/Pure/drule.ML	Fri Nov 26 22:04:33 2010 +0100
+++ b/src/Pure/drule.ML	Fri Nov 26 22:29:41 2010 +0100
@@ -891,7 +891,7 @@
         handle TYPE (msg, _, _) => err msg;
 
     fun zip_vars xs ys =
-      zip_options xs ys handle Library.UnequalLengths =>
+      zip_options xs ys handle ListPair.UnequalLengths =>
         err "more instantiations than variables in thm";
 
     (*instantiate types first!*)

--- a/src/Pure/library.ML	Fri Nov 26 22:04:33 2010 +0100
+++ b/src/Pure/library.ML	Fri Nov 26 22:29:41 2010 +0100
@@ -58,7 +58,6 @@
   val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
 
   (*lists*)
-  exception UnequalLengths
   val single: 'a -> 'a list
   val the_single: 'a list -> 'a
   val singleton: ('a list -> 'b list) -> 'a -> 'b
@@ -322,8 +321,6 @@
 
 (** lists **)
 
-exception UnequalLengths;
-
 fun single x = [x];
 
 fun the_single [x] = x
@@ -496,7 +493,7 @@
       let val (ps, qs) = chop (length xs) ys
       in ps :: unflat xss qs end
   | unflat [] [] = []
-  | unflat _ _ = raise UnequalLengths;
+  | unflat _ _ = raise ListPair.UnequalLengths;
 
 fun burrow f xss = unflat xss (f (flat xss));
 
@@ -535,19 +532,17 @@
 
 (* lists of pairs *)
 
-exception UnequalLengths;
-
 fun map2 _ [] [] = []
   | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys
-  | map2 _ _ _ = raise UnequalLengths;
+  | map2 _ _ _ = raise ListPair.UnequalLengths;
 
 fun fold2 f [] [] z = z
   | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z)
-  | fold2 f _ _ _ = raise UnequalLengths;
+  | fold2 f _ _ _ = raise ListPair.UnequalLengths;
 
 fun fold_rev2 f [] [] z = z
   | fold_rev2 f (x :: xs) (y :: ys) z = f x y (fold_rev2 f xs ys z)
-  | fold_rev2 f _ _ _ = raise UnequalLengths;
+  | fold_rev2 f _ _ _ = raise ListPair.UnequalLengths;
 
 fun forall2 P [] [] = true
   | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
@@ -563,13 +558,13 @@
 fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys
   | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys
   | zip_options _ [] = []
-  | zip_options [] _ = raise UnequalLengths;
+  | zip_options [] _ = raise ListPair.UnequalLengths;
 
 (*combine two lists forming a list of pairs:
   [x1, ..., xn] ~~ [y1, ..., yn]  ===>  [(x1, y1), ..., (xn, yn)]*)
 fun [] ~~ [] = []
   | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys)
-  | _ ~~ _ = raise UnequalLengths;
+  | _ ~~ _ = raise ListPair.UnequalLengths;
 
 (*inverse of ~~; the old 'split':
   [(x1, y1), ..., (xn, yn)]  ===>  ([x1, ..., xn], [y1, ..., yn])*)
@@ -848,10 +843,11 @@
 
 fun map_transpose f xss =
   let
-    val n = case distinct (op =) (map length xss)
-     of [] => 0
+    val n =
+      (case distinct (op =) (map length xss) of
+        [] => 0
       | [n] => n
-      | _ => raise UnequalLengths;
+      | _ => raise ListPair.UnequalLengths);
   in map_range (fn m => f (map (fn xs => nth xs m) xss)) n end;
 
 
@@ -1071,3 +1067,5 @@
 
 structure Basic_Library: BASIC_LIBRARY = Library;
 open Basic_Library;
+
+datatype legacy = UnequalLengths;

--- a/src/Pure/pattern.ML	Fri Nov 26 22:04:33 2010 +0100
+++ b/src/Pure/pattern.ML	Fri Nov 26 22:29:41 2010 +0100
@@ -365,7 +365,7 @@
   and cases(binders,env as (iTs,itms),pat,obj) =
     let val (ph,pargs) = strip_comb pat
         fun rigrig1(iTs,oargs) = fold (mtch binders) (pargs~~oargs) (iTs,itms)
-				 handle UnequalLengths => raise MATCH
+				 handle ListPair.UnequalLengths => raise MATCH
         fun rigrig2((a:string,Ta),(b,Tb),oargs) =
               if a <> b then raise MATCH
               else rigrig1(typ_match thy (Ta,Tb) iTs, oargs)

--- a/src/Tools/eqsubst.ML	Fri Nov 26 22:04:33 2010 +0100
+++ b/src/Tools/eqsubst.ML	Fri Nov 26 22:29:41 2010 +0100
@@ -235,13 +235,13 @@
           val initenv =
             Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
           val useq = Unify.smash_unifiers thry [a] initenv
-              handle UnequalLengths => Seq.empty
+              handle ListPair.UnequalLengths => Seq.empty
                    | Term.TERM _ => Seq.empty;
           fun clean_unify' useq () =
               (case (Seq.pull useq) of
                  NONE => NONE
                | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
-              handle UnequalLengths => NONE
+              handle ListPair.UnequalLengths => NONE
                    | Term.TERM _ => NONE
         in
           (Seq.make (clean_unify' useq))

--- a/src/Tools/induct_tacs.ML	Fri Nov 26 22:04:33 2010 +0100
+++ b/src/Tools/induct_tacs.ML	Fri Nov 26 22:29:41 2010 +0100
@@ -96,7 +96,7 @@
     val _ = Method.trace ctxt [rule'];
 
     val concls = Logic.dest_conjunctions (Thm.concl_of rule);
-    val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
+    val insts = maps prep_inst (concls ~~ varss) handle ListPair.UnequalLengths =>
       error "Induction rule has different numbers of variables";
   in res_inst_tac ctxt insts rule' i st end
   handle THM _ => Seq.empty;