# HG changeset patch
# User huffman
# Date 1290815399 28800
# Node ID 35781a159d1cc9bf06e119caf589e5aeb84b28f9
# Parent  2037021f034f1cb75f7a5c8aa570bf1ab0b55e19# Parent  a71f786d20da9103006db08007a36bef2e3f37c3
merged

diff -r 2037021f034f -r 35781a159d1c NEWS
--- a/NEWS	Fri Nov 26 15:24:11 2010 -0800
+++ b/NEWS	Fri Nov 26 15:49:59 2010 -0800
@@ -104,14 +104,13 @@
 avoid confusion with finite sets.  INCOMPATIBILITY.
 
 * Quickcheck's generator for random generation is renamed from "code" to
-"random".  INCOMPATIBILITY. 
+"random".  INCOMPATIBILITY.
 
 * Theory Multiset provides stable quicksort implementation of sort_key.
 
 * Quickcheck now has a configurable time limit which is set to 30 seconds
 by default. This can be changed by adding [timeout = n] to the quickcheck
-command. The time limit for auto quickcheck is still set independently,
-by default to 5 seconds.
+command. The time limit for Auto Quickcheck is still set independently.
 
 * New command 'partial_function' provides basic support for recursive
 function definitions over complete partial orders. Concrete instances
@@ -357,11 +356,26 @@
     (and "ms" and "min" are no longer supported)
     INCOMPATIBILITY.
 
+* Metis and Meson now have configuration options "meson_trace", "metis_trace",
+  and "metis_verbose" that can be enabled to diagnose these tools. E.g.
+
+    using [[metis_trace = true]]
+
 * Nitpick:
   - Renamed options:
     nitpick [timeout = 77 s] ~> nitpick [timeout = 77]
     nitpick [tac_timeout = 777 ms] ~> nitpick [tac_timeout = 0.777]
     INCOMPATIBILITY.
+  - Now requires Kodkodi 1.2.9. INCOMPATIBILITY.
+  - Added support for partial quotient types.
+  - Added local versions of the "Nitpick.register_xxx" functions.
+  - Added "whack" option.
+  - Allow registration of quotient types as codatatypes.
+  - Improved "merge_type_vars" option to merge more types.
+  - Removed unsound "fast_descrs" option.
+  - Added custom symmetry breaking for datatypes, making it possible to reach
+    higher cardinalities.
+  - Prevent the expansion of too large definitions.
 
 * Changed SMT configuration options:
   - Renamed:
@@ -507,6 +521,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.
@@ -650,7 +667,7 @@
 
 Tracing is then active for all invocations of the simplifier in
 subsequent goal refinement steps. Tracing may also still be enabled or
-disabled via the ProofGeneral settings menu.
+disabled via the Proof General settings menu.
 
 * Separate commands 'hide_class', 'hide_type', 'hide_const',
 'hide_fact' replace the former 'hide' KIND command.  Minor
diff -r 2037021f034f -r 35781a159d1c doc-src/LaTeXsugar/Sugar/document/root.tex
--- a/doc-src/LaTeXsugar/Sugar/document/root.tex	Fri Nov 26 15:24:11 2010 -0800
+++ b/doc-src/LaTeXsugar/Sugar/document/root.tex	Fri Nov 26 15:49:59 2010 -0800
@@ -3,23 +3,7 @@
 
 % further packages required for unusual symbols (see also isabellesym.sty)
 % use only when needed
-\usepackage{amssymb}                  % for \<leadsto>, \<box>, \<diamond>,
-                                       % \<sqsupset>, \<mho>, \<Join>, 
-                                       % \<lhd>, \<lesssim>, \<greatersim>,
-                                       % \<lessapprox>, \<greaterapprox>,
-                                       % \<triangleq>, \<yen>, \<lozenge>
-%\usepackage[greek,english]{babel}     % greek for \<euro>,
-                                       % english for \<guillemotleft>, 
-                                       %             \<guillemotright>
-                                       % default language = last
-%\usepackage[latin1]{inputenc}         % for \<onesuperior>, \<onequarter>,
-                                       % \<twosuperior>, \<onehalf>,
-                                       % \<threesuperior>, \<threequarters>,
-                                       % \<degree>
-%\usepackage[only,bigsqcap]{stmaryrd}  % for \<Sqinter>
-%\usepackage{eufrak}                   % for \<AA> ... \<ZZ>, \<aa> ... \<zz>
-                                       % (only needed if amssymb not used)
-%\usepackage{textcomp}                 % for \<cent>, \<currency>
+\usepackage{amssymb}
 
 \usepackage{mathpartir}
 
diff -r 2037021f034f -r 35781a159d1c doc-src/Main/main.tex
--- a/doc-src/Main/main.tex	Fri Nov 26 15:24:11 2010 -0800
+++ b/doc-src/Main/main.tex	Fri Nov 26 15:49:59 2010 -0800
@@ -9,31 +9,8 @@
 \textheight=234mm
 
 \usepackage{../isabelle,../isabellesym}
-
-% further packages required for unusual symbols (see also
-% isabellesym.sty), use only when needed
-
 \usepackage{amssymb}
-  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
-  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
-  %\<triangleq>, \<yen>, \<lozenge>
-
-%\usepackage[greek,english]{babel}
-  %option greek for \<euro>
-  %option english (default language) for \<guillemotleft>, \<guillemotright>
-
-%\usepackage[latin1]{inputenc}
-  %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
-  %\<threesuperior>, \<threequarters>, \<degree>
-
 \usepackage[only,bigsqcap]{stmaryrd}
-  %for \<Sqinter>
-
-%\usepackage{eufrak}
-  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
-
-%\usepackage{textcomp}
-  %for \<cent>, \<currency>
 
 % this should be the last package used
 \usepackage{../pdfsetup}
diff -r 2037021f034f -r 35781a159d1c src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Fun.thy	Fri Nov 26 15:49:59 2010 -0800
@@ -155,11 +155,6 @@
   shows "inj f"
   using assms unfolding inj_on_def by auto
 
-text{*For Proofs in @{text "Tools/Datatype/datatype_rep_proofs"}*}
-lemma datatype_injI:
-    "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)"
-by (simp add: inj_on_def)
-
 theorem range_ex1_eq: "inj f \<Longrightarrow> b : range f = (EX! x. b = f x)"
   by (unfold inj_on_def, blast)
 
diff -r 2037021f034f -r 35781a159d1c src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -103,11 +103,6 @@
 
 fun iszero (k,r) = r =/ rat_0;
 
-fun fold_rev2 f l1 l2 b =
-  case (l1,l2) of
-    ([],[]) => b
-  | (h1::t1,h2::t2) => f h1 h2 (fold_rev2 f t1 t2 b)
-  | _ => error "fold_rev2";
 
 (* Vectors. Conventionally indexed 1..n.                                     *)
 
diff -r 2037021f034f -r 35781a159d1c src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Nov 26 15:49:59 2010 -0800
@@ -19,7 +19,7 @@
 lemma injective_scaleR: 
 assumes "(c :: real) ~= 0"
 shows "inj (%(x :: 'n::euclidean_space). scaleR c x)"
-by (metis assms datatype_injI injI real_vector.scale_cancel_left)
+  by (metis assms injI real_vector.scale_cancel_left)
 
 lemma linear_add_cmul:
 fixes f :: "('m::euclidean_space) => ('n::euclidean_space)" 
diff -r 2037021f034f -r 35781a159d1c src/HOL/Multivariate_Analysis/normarith.ML
--- a/src/HOL/Multivariate_Analysis/normarith.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Multivariate_Analysis/normarith.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -117,13 +117,6 @@
   [] => []
 | h::t => map (cons h) (combinations (k - 1) t) @ combinations k t
 
-
-fun forall2 p l1 l2 = case (l1,l2) of
-   ([],[]) => true
- | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2
- | _ => false;
-
-
 fun vertices vs eqs =
  let
   fun vertex cmb = case solve(vs,cmb) of
@@ -131,16 +124,16 @@
    | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v Rat.zero) vs)
   val rawvs = map_filter vertex (combinations (length vs) eqs)
   val unset = filter (forall (fn c => c >=/ Rat.zero)) rawvs
- in fold_rev (insert (uncurry (forall2 (curry op =/)))) unset []
+ in fold_rev (insert (eq_list op =/)) unset []
  end
 
-fun subsumes l m = forall2 (fn x => fn y => Rat.abs x <=/ Rat.abs y) l m
+val subsumes = eq_list (fn (x, y) => Rat.abs x <=/ Rat.abs y)
 
 fun subsume todo dun = case todo of
  [] => dun
 |v::ovs =>
-   let val dun' = if exists (fn w => subsumes w v) dun then dun
-                  else v::(filter (fn w => not(subsumes v w)) dun)
+   let val dun' = if exists (fn w => subsumes (w, v)) dun then dun
+                  else v:: filter (fn w => not (subsumes (v, w))) dun
    in subsume ovs dun'
    end;
 
@@ -246,10 +239,6 @@
   Const(@{const_name norm},_)$_ => arg_conv vector_canon_conv ct
  | _ => raise CTERM ("norm_canon_conv", [ct])
 
-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;
-
 fun int_flip v eq =
   if FuncUtil.Intfunc.defined eq v
   then FuncUtil.Intfunc.update (v, Rat.neg (FuncUtil.Intfunc.apply eq v)) eq else eq;
diff -r 2037021f034f -r 35781a159d1c src/HOL/Statespace/document/root.tex
--- a/src/HOL/Statespace/document/root.tex	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Statespace/document/root.tex	Fri Nov 26 15:49:59 2010 -0800
@@ -1,31 +1,5 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
-
-% further packages required for unusual symbols (see also
-% isabellesym.sty), use only when needed
-
-%\usepackage{amssymb}
-  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
-  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
-  %\<triangleq>, \<yen>, \<lozenge>
-
-%\usepackage[greek,english]{babel}
-  %option greek for \<euro>
-  %option english (default language) for \<guillemotleft>, \<guillemotright>
-
-%\usepackage[latin1]{inputenc}
-  %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
-  %\<threesuperior>, \<threequarters>, \<degree>
-
-%\usepackage[only,bigsqcap]{stmaryrd}
-  %for \<Sqinter>
-
-%\usepackage{eufrak}
-  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
-
-%\usepackage{textcomp}
-  %for \<cent>, \<currency>
-
 % this should be the last package used
 \usepackage{pdfsetup}
 
diff -r 2037021f034f -r 35781a159d1c src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -54,6 +54,8 @@
 val Suml_inject = @{thm Suml_inject};
 val Sumr_inject = @{thm Sumr_inject};
 
+val datatype_injI =
+  @{lemma "(!!x. ALL y. f x = f y --> x = y) ==> inj f" by (simp add: inj_on_def)};
 
 
 (** proof of characteristic theorems **)
@@ -438,8 +440,7 @@
                              Lim_inject :: inj_thms') @ fun_congs) 1),
                          atac 1]))])])])]);
 
-        val inj_thms'' = map (fn r => r RS @{thm datatype_injI})
-                             (split_conj_thm inj_thm);
+        val inj_thms'' = map (fn r => r RS datatype_injI) (split_conj_thm inj_thm);
 
         val elem_thm = 
             Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
diff -r 2037021f034f -r 35781a159d1c src/HOL/Tools/Datatype/datatype_aux.ML
--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -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,
diff -r 2037021f034f -r 35781a159d1c src/HOL/Tools/Datatype/datatype_prop.ML
--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -48,8 +48,8 @@
 
 fun make_tnames Ts =
   let
-    fun type_name (TFree (name, _)) = implode (tl (raw_explode name))  (* FIXME Symbol.explode (?) *)
-      | type_name (Type (name, _)) = 
+    fun type_name (TFree (name, _)) = unprefix "'" name
+      | type_name (Type (name, _)) =
           let val name' = Long_Name.base_name name
           in if Syntax.is_identifier name' then name' else "x" end;
   in indexify_names (map type_name Ts) end;
diff -r 2037021f034f -r 35781a159d1c src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Tools/Function/function_lib.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -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;
 
 
 
diff -r 2037021f034f -r 35781a159d1c src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Tools/Function/size.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -71,7 +71,7 @@
     val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
       map (fn T as TFree (s, _) =>
         let
-          val name = "f" ^ implode (tl (raw_explode s));  (* FIXME Symbol.explode (?) *)
+          val name = "f" ^ unprefix "'" s;
           val U = T --> HOLogic.natT
         in
           (((s, Free (name, U)), U), name)
diff -r 2037021f034f -r 35781a159d1c src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Tools/Meson/meson.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -46,7 +46,7 @@
 structure Meson : MESON =
 struct
 
-val (trace, trace_setup) = Attrib.config_bool "trace_meson" (K false)
+val (trace, trace_setup) = Attrib.config_bool "meson_trace" (K false)
 
 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
 
diff -r 2037021f034f -r 35781a159d1c src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -31,8 +31,8 @@
 
 open Metis_Translate
 
-val (trace, trace_setup) = Attrib.config_bool "trace_metis" (K false)
-val (verbose, verbose_setup) = Attrib.config_bool "verbose_metis" (K true)
+val (trace, trace_setup) = Attrib.config_bool "metis_trace" (K false)
+val (verbose, verbose_setup) = Attrib.config_bool "metis_verbose" (K true)
 
 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
 fun verbose_warning ctxt msg =
diff -r 2037021f034f -r 35781a159d1c src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -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 *)
diff -r 2037021f034f -r 35781a159d1c src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -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)
diff -r 2037021f034f -r 35781a159d1c src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -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
diff -r 2037021f034f -r 35781a159d1c src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -440,7 +440,7 @@
 val smt_iter_timeout_divisor = 2
 val smt_monomorph_limit = 4
 
-fun smt_filter_loop ({debug, verbose, timeout, ...} : params) remote state i =
+fun smt_filter_loop ({verbose, timeout, ...} : params) remote state i =
   let
     val ctxt = Proof.context_of state
     fun iter timeout iter_num outcome0 msecs_so_far facts =
@@ -534,6 +534,7 @@
     val smt_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated
     val {outcome, used_facts, run_time_in_msecs} =
       smt_filter_loop params remote state subgoal (map_filter smt_fact facts)
+    val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
     val outcome = outcome |> Option.map failure_from_smt_failure
     val message =
       case outcome of
@@ -547,8 +548,9 @@
         in
           try_command_line (proof_banner auto)
                            (apply_on_subgoal subgoal subgoal_count ^
-                            command_call method (map (fst o fst) used_facts)) ^
-          minimize_line minimize_command (map (fst o fst) used_facts)
+                            command_call method (map fst other_lemmas)) ^
+          minimize_line minimize_command
+                        (map fst (other_lemmas @ chained_lemmas))
         end
       | SOME failure => string_for_failure "SMT solver" failure
   in
diff -r 2037021f034f -r 35781a159d1c src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -24,7 +24,9 @@
   val command_call : string -> string list -> string
   val try_command_line : string -> string -> string
   val minimize_line : ('a list -> string) -> 'a list -> string
-  val metis_proof_text : metis_params -> text_result
+  val split_used_facts :
+    (string * locality) list
+    -> (string * locality) list * (string * locality) list
   val isar_proof_text : isar_params -> metis_params -> text_result
   val proof_text : bool -> isar_params -> metis_params -> text_result
 end;
@@ -159,15 +161,15 @@
 fun used_facts_in_tstplike_proof fact_names =
   atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact fact_names)
 
-fun used_facts fact_names =
-  used_facts_in_tstplike_proof fact_names
-  #> List.partition (curry (op =) Chained o snd)
+val split_used_facts =
+  List.partition (curry (op =) Chained o snd)
   #> pairself (sort_distinct (string_ord o pairself fst))
 
 fun metis_proof_text (banner, full_types, minimize_command,
                       tstplike_proof, fact_names, goal, i) =
   let
-    val (chained_lemmas, other_lemmas) = used_facts fact_names tstplike_proof
+    val (chained_lemmas, other_lemmas) =
+      split_used_facts (used_facts_in_tstplike_proof fact_names tstplike_proof)
     val n = Logic.count_prems (prop_of goal)
   in
     (metis_line banner full_types i n (map fst other_lemmas) ^
@@ -912,14 +914,14 @@
   in do_proof end
 
 fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
-                    (other_params as (_, full_types, _, tstplike_proof,
+                    (metis_params as (_, full_types, _, tstplike_proof,
                                       fact_names, goal, i)) =
   let
     val (params, hyp_ts, concl_t) = strip_subgoal goal i
     val frees = fold Term.add_frees (concl_t :: hyp_ts) []
     val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
     val n = Logic.count_prems (prop_of goal)
-    val (one_line_proof, lemma_names) = metis_proof_text other_params
+    val (one_line_proof, lemma_names) = metis_proof_text metis_params
     fun isar_proof_for () =
       case isar_proof_from_tstplike_proof pool ctxt full_types tfrees
                isar_shrink_factor tstplike_proof conjecture_shape fact_names
@@ -940,8 +942,8 @@
         |> the_default "\nWarning: The Isar proof construction failed."
   in (one_line_proof ^ isar_proof, lemma_names) end
 
-fun proof_text isar_proof isar_params other_params =
+fun proof_text isar_proof isar_params metis_params =
   (if isar_proof then isar_proof_text isar_params else metis_proof_text)
-      other_params
+      metis_params
 
 end;
diff -r 2037021f034f -r 35781a159d1c src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Tools/code_evaluation.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -54,7 +54,7 @@
 
 (* code equations for datatypes *)
 
-fun mk_term_of_eq thy ty (c, tys) =
+fun mk_term_of_eq thy ty (c, (_, tys)) =
   let
     val t = list_comb (Const (c, tys ---> ty),
       map Free (Name.names Name.context "a" tys));
@@ -74,7 +74,7 @@
     val vs = map (fn (v, sort) =>
       (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
     val ty = Type (tyco, map TFree vs);
-    val cs = (map o apsnd o map o map_atyps)
+    val cs = (map o apsnd o apsnd o map o map_atyps)
       (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
     val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
     val eqs = map (mk_term_of_eq thy ty) cs;
@@ -121,7 +121,7 @@
     |> Code.add_eqn eq
   end;
 
-fun ensure_abs_term_of_code (tyco, (raw_vs, ((abs, ty), (proj, _)))) thy =
+fun ensure_abs_term_of_code (tyco, (raw_vs, ((abs, (_, ty)), (proj, _)))) thy =
   let
     val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
   in if has_inst then add_abs_term_of_code tyco raw_vs abs ty proj thy else thy end;
diff -r 2037021f034f -r 35781a159d1c src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Tools/groebner.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -233,14 +233,9 @@
 
 fun align  ((p,hp),(q,hq)) =
   if poly_lt p q then ((p,hp),(q,hq)) else ((q,hq),(p,hp));
-fun forall2 p l1 l2 =
-  case (l1,l2) of
-    ([],[]) => true
-  | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2
-  | _ => false;
 
 fun poly_eq p1 p2 =
-  forall2 (fn (c1,m1) => fn (c2,m2) => c1 =/ c2 andalso (m1: int list) = m2) p1 p2;
+  eq_list (fn ((c1, m1), (c2, m2)) => c1 =/ c2 andalso (m1: int list) = m2) (p1, p2);
 
 fun memx ((p1,h1),(p2,h2)) ppairs =
   not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs);
diff -r 2037021f034f -r 35781a159d1c src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Tools/record.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -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)]);
diff -r 2037021f034f -r 35781a159d1c src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/Tools/refute.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -2953,9 +2953,7 @@
 fun stlc_printer ctxt model T intr assignment =
   let
     (* string -> string *)
-    fun strip_leading_quote s =
-      (implode o (fn [] => [] | x::xs => if x="'" then xs else x::xs)
-        o raw_explode) s  (* FIXME Symbol.explode (?) *)
+    val strip_leading_quote = perhaps (try (unprefix "'"))
     (* Term.typ -> string *)
     fun string_of_typ (Type (s, _)) = s
       | string_of_typ (TFree (x, _)) = strip_leading_quote x
diff -r 2037021f034f -r 35781a159d1c src/HOL/ex/Normalization_by_Evaluation.thy
--- a/src/HOL/ex/Normalization_by_Evaluation.thy	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/HOL/ex/Normalization_by_Evaluation.thy	Fri Nov 26 15:49:59 2010 -0800
@@ -66,7 +66,7 @@
 lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization
 
 lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
-  by normalization rule+
+  by normalization
 lemma "rev [a, b, c] = [c, b, a]" by normalization
 value [nbe] "rev (a#b#cs) = rev cs @ [b, a]"
 value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
@@ -108,10 +108,13 @@
 lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
 value [nbe] "Suc 0 \<in> set ms"
 
+(* non-left-linear patterns, equality by extensionality *)
+
 lemma "f = f" by normalization
 lemma "f x = f x" by normalization
 lemma "(f o g) x = f (g x)" by normalization
 lemma "(f o id) x = f x" by normalization
+lemma "(id :: bool \<Rightarrow> bool) = id" by normalization
 value [nbe] "(\<lambda>x. x)"
 
 (* Church numerals: *)
diff -r 2037021f034f -r 35781a159d1c src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/Pure/Isar/code.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -21,7 +21,7 @@
 
   (*constructor sets*)
   val constrset_of_consts: theory -> (string * typ) list
-    -> string * ((string * sort) list * (string * typ list) list)
+    -> string * ((string * sort) list * (string * ((string * sort) list * typ list)) list)
 
   (*code equations and certificates*)
   val mk_eqn: theory -> thm * bool -> thm * bool
@@ -48,11 +48,11 @@
   val add_datatype: (string * typ) list -> theory -> theory
   val add_datatype_cmd: string list -> theory -> theory
   val datatype_interpretation:
-    (string * ((string * sort) list * (string * typ list) list)
+    (string * ((string * sort) list * (string * ((string * sort) list * typ list)) list)
       -> theory -> theory) -> theory -> theory
   val add_abstype: thm -> theory -> theory
   val abstype_interpretation:
-    (string * ((string * sort) list * ((string * typ) * (string * thm)))
+    (string * ((string * sort) list * ((string * ((string * sort) list * typ)) * (string * thm)))
       -> theory -> theory) -> theory -> theory
   val add_eqn: thm -> theory -> theory
   val add_nbe_eqn: thm -> theory -> theory
@@ -66,7 +66,8 @@
   val del_eqns: string -> theory -> theory
   val add_case: thm -> theory -> theory
   val add_undefined: string -> theory -> theory
-  val get_type: theory -> string -> ((string * sort) list * ((string * string list) * typ list) list)
+  val get_type: theory -> string
+    -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool
   val get_type_of_constr_or_abstr: theory -> string -> (string * bool) option
   val is_constr: theory -> string -> bool
   val is_abstr: theory -> string -> bool
@@ -147,11 +148,11 @@
 
 (* datatypes *)
 
-datatype typ_spec = Constructors of (string * typ list) list
-  | Abstractor of (string * typ) * (string * thm);
+datatype typ_spec = Constructors of (string * ((string * sort) list * typ list)) list
+  | Abstractor of (string * ((string * sort) list * typ)) * (string * thm);
 
 fun constructors_of (Constructors cos) = (cos, false)
-  | constructors_of (Abstractor ((co, ty), _)) = ([(co, [ty])], true);
+  | constructors_of (Abstractor ((co, (vs, ty)), _)) = ([(co, (vs, [ty]))], true);
 
 
 (* functions *)
@@ -412,7 +413,8 @@
       let
         val the_v = the o AList.lookup (op =) (vs ~~ vs');
         val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty;
-      in (c, (fst o strip_type) ty') end;
+        val vs'' = map dest_TFree (Sign.const_typargs thy (c, ty'));
+      in (c, (vs'', (fst o strip_type) ty')) end;
     val c' :: cs' = map (ty_sorts thy) cs;
     val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
     val vs = Name.names Name.context Name.aT sorts;
@@ -423,7 +425,7 @@
  of (_, entry) :: _ => SOME entry
   | _ => NONE;
 
-fun get_type_spec thy tyco = case get_type_entry thy tyco
+fun get_type thy tyco = case get_type_entry thy tyco
  of SOME (vs, spec) => apfst (pair vs) (constructors_of spec)
   | NONE => arity_number thy tyco
       |> Name.invents Name.context Name.aT
@@ -435,17 +437,9 @@
  of SOME (vs, Abstractor spec) => (vs, spec)
   | _ => error ("Not an abstract type: " ^ tyco);
  
-fun get_type thy tyco =
-  let
-    val ((vs, cos), _) = get_type_spec thy tyco;
-    fun args_of c tys = map (fst o dest_TFree)
-      (Sign.const_typargs thy (c, tys ---> Type (tyco, map TFree vs)));
-    fun add_typargs (c, tys) = ((c, args_of c tys), tys);
-  in (vs, map add_typargs cos) end;
-
 fun get_type_of_constr_or_abstr thy c =
   case (snd o strip_type o const_typ thy) c
-   of Type (tyco, _) => let val ((vs, cos), abstract) = get_type_spec thy tyco
+   of Type (tyco, _) => let val ((vs, cos), abstract) = get_type thy tyco
         in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end
     | _ => NONE;
 
@@ -683,8 +677,9 @@
     val _ = if param = rhs then () else bad "Not an abstype certificate";
     val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy (abs, Logic.unvarifyT_global raw_ty);
     val ty = domain_type ty';
+    val vs' = map dest_TFree (Sign.const_typargs thy (abs, ty'));
     val ty_abs = range_type ty';
-  in (tyco, (vs ~~ sorts, ((abs, ty), (rep, thm)))) end;
+  in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end;
 
 
 (* code equation certificates *)
@@ -784,7 +779,7 @@
 
 fun cert_of_proj thy c tyco =
   let
-    val (vs, ((abs, ty), (rep, cert))) = get_abstype_spec thy tyco;
+    val (vs, ((abs, (_, ty)), (rep, cert))) = get_abstype_spec thy tyco;
     val _ = if c = rep then () else
       error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy rep);
   in Projection (mk_proj tyco vs ty abs rep, tyco) end;
@@ -979,8 +974,8 @@
         pretty_typ typ
         :: Pretty.str "="
         :: (if abstract then [Pretty.str "(abstract)"] else [])
-        @ separate (Pretty.str "|") (map (fn (c, []) => Pretty.str (string_of_const thy c)
-             | (c, tys) =>
+        @ separate (Pretty.str "|") (map (fn (c, (_, [])) => Pretty.str (string_of_const thy c)
+             | (c, (_, tys)) =>
                  (Pretty.block o Pretty.breaks)
                     (Pretty.str (string_of_const thy c)
                       :: Pretty.str "of"
@@ -1202,7 +1197,7 @@
   Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
 
 fun datatype_interpretation f = Datatype_Interpretation.interpretation
-  (fn (tyco, _) => fn thy => f (tyco, fst (get_type_spec thy tyco)) thy);
+  (fn (tyco, _) => fn thy => f (tyco, fst (get_type thy tyco)) thy);
 
 fun add_datatype proto_constrs thy =
   let
@@ -1226,7 +1221,7 @@
 
 fun add_abstype proto_thm thy =
   let
-    val (tyco, (vs, (abs_ty as (abs, ty), (rep, cert)))) =
+    val (tyco, (vs, (abs_ty as (abs, (_, ty)), (rep, cert)))) =
       error_thm (check_abstype_cert thy) proto_thm;
   in
     thy
diff -r 2037021f034f -r 35781a159d1c src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/Pure/Proof/reconstruct.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -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;
 
diff -r 2037021f034f -r 35781a159d1c src/Pure/consts.ML
--- a/src/Pure/consts.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/Pure/consts.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -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;
 
diff -r 2037021f034f -r 35781a159d1c src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/Pure/drule.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -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!*)
diff -r 2037021f034f -r 35781a159d1c src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/Pure/library.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -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
@@ -97,6 +96,7 @@
   val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
+  val fold_rev2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
   val forall2: ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
   val zip_options: 'a list -> 'b option list -> ('a * 'b) list
   val ~~ : 'a list * 'b list -> ('a * 'b) list
@@ -321,8 +321,6 @@
 
 (** lists **)
 
-exception UnequalLengths;
-
 fun single x = [x];
 
 fun the_single [x] = x
@@ -495,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));
 
@@ -534,19 +532,21 @@
 
 (* 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 ListPair.UnequalLengths;
 
 fun forall2 P [] [] = true
   | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
-  | forall2 P _ _ = false;
+  | forall2 P _ _ = raise ListPair.UnequalLengths;
 
 fun map_split f [] = ([], [])
   | map_split f (x :: xs) =
@@ -558,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])*)
@@ -843,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;
 
 
@@ -1066,3 +1067,5 @@
 
 structure Basic_Library: BASIC_LIBRARY = Library;
 open Basic_Library;
+
+datatype legacy = UnequalLengths;
diff -r 2037021f034f -r 35781a159d1c src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/Pure/pattern.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -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)
diff -r 2037021f034f -r 35781a159d1c src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/Tools/Code/code_runtime.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -258,7 +258,7 @@
 
 fun check_datatype thy tyco some_consts =
   let
-    val constrs = (map (fst o fst) o snd o Code.get_type thy) tyco;
+    val constrs = (map fst o snd o fst o Code.get_type thy) tyco;
     val _ = case some_consts
      of SOME consts =>
           let
diff -r 2037021f034f -r 35781a159d1c src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/Tools/Code/code_thingol.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -573,12 +573,12 @@
 
 fun ensure_tyco thy algbr eqngr permissive tyco =
   let
-    val (vs, cos) = Code.get_type thy tyco;
+    val ((vs, cos), _) = Code.get_type thy tyco;
     val stmt_datatype =
       fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
-      ##>> fold_map (fn ((c, vs), tys) =>
+      ##>> fold_map (fn (c, (vs, tys)) =>
         ensure_const thy algbr eqngr permissive c
-        ##>> pair (map (unprefix "'") vs)
+        ##>> pair (map (unprefix "'" o fst) vs)
         ##>> fold_map (translate_typ thy algbr eqngr permissive) tys) cos
       #>> (fn info => Datatype (tyco, info));
   in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
diff -r 2037021f034f -r 35781a159d1c src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/Tools/eqsubst.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -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))
diff -r 2037021f034f -r 35781a159d1c src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/Tools/induct_tacs.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -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;
diff -r 2037021f034f -r 35781a159d1c src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Fri Nov 26 15:24:11 2010 -0800
+++ b/src/Tools/nbe.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -18,7 +18,7 @@
   val apps: Univ -> Univ list -> Univ        (*explicit applications*)
   val abss: int -> (Univ list -> Univ) -> Univ
                                              (*abstractions as closures*)
-  val same: Univ -> Univ -> bool
+  val eq_Univ: Univ * Univ -> bool
 
   val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context
   val trace: bool Unsynchronized.ref
@@ -170,11 +170,6 @@
   | Abs of (int * (Univ list -> Univ)) * Univ list
                                        (*abstractions as closures*);
 
-fun same (Const (k, xs)) (Const (l, ys)) = k = l andalso forall2 same xs ys
-  | same (DFree (s, k)) (DFree (t, l)) = s = t andalso k = l
-  | same (BVar (k, xs)) (BVar (l, ys)) = k = l andalso forall2 same xs ys
-  | same _ _ = false;
-
 
 (* constructor functions *)
 
@@ -188,6 +183,28 @@
   | apps (Const (name, xs)) ys = Const (name, ys @ xs)
   | apps (BVar (n, xs)) ys = BVar (n, ys @ xs);
 
+fun satisfy_abs (abs as ((n, f), xs)) some_k =
+  let
+    val ys = case some_k
+     of NONE => replicate n (BVar (0, []))
+      | SOME k => map_range (fn l => BVar (k + l, [])) n;
+  in (apps (Abs abs) ys, ys) end;
+
+fun maxidx (Const (_, xs)) = fold maxidx xs
+  | maxidx (DFree _) = I
+  | maxidx (BVar (l, xs)) = fold maxidx xs #> Integer.max (l + 1)
+  | maxidx (Abs abs) = maxidx (fst (satisfy_abs abs NONE));
+
+fun eq_Univ (Const (k, xs), Const (l, ys)) = k = l andalso eq_list eq_Univ (xs, ys)
+  | eq_Univ (DFree (s, k), DFree (t, l)) = s = t andalso k = l
+  | eq_Univ (BVar (k, xs), BVar (l, ys)) = k = l andalso eq_list eq_Univ (xs, ys)
+  | eq_Univ (x as Abs abs, y) =
+      let
+        val (x, ys) = satisfy_abs abs ((SOME o maxidx x o maxidx y) 0)
+      in eq_Univ (x, apps y ys) end
+  | eq_Univ (x, y as Abs _) = eq_Univ (y, x)
+  | eq_Univ _ = false;
+
 
 (** assembling and compiling ML code from terms **)
 
@@ -241,7 +258,7 @@
   val name_const =  prefix ^ "Const";
   val name_abss =   prefix ^ "abss";
   val name_apps =   prefix ^ "apps";
-  val name_same =   prefix ^ "same";
+  val name_eq =     prefix ^ "eq_Univ";
 in
 
 val univs_cookie = (Univs.get, put_result, name_put);
@@ -267,7 +284,7 @@
 fun nbe_abss 0 f = f `$` ml_list []
   | nbe_abss n f = name_abss `$$` [string_of_int n, f];
 
-fun nbe_same v1 v2 = "(" ^ name_same ^ " " ^ nbe_bound v1 ^ " " ^ nbe_bound v2 ^ ")";
+fun nbe_eq (v1, v2) = "(" ^ name_eq ^ " (" ^ nbe_bound v1 ^ ", " ^ nbe_bound v2 ^ "))";
 
 end;
 
@@ -353,7 +370,7 @@
         val (samepairs, args') = subst_nonlin_vars args;
         val s_args = map assemble_arg args';
         val s_rhs = if null samepairs then assemble_rhs rhs
-          else ml_if (ml_and (map (uncurry nbe_same) samepairs))
+          else ml_if (ml_and (map nbe_eq samepairs))
             (assemble_rhs rhs) default_rhs;
         val eqns = if is_eval then
             [([ml_list (rev (dicts @ s_args))], s_rhs)]