# HG changeset patch
# User panny
# Date 1385477643 -3600
# Node ID 5836854ca0a8027acf3faa79339b5ee8b840ef42
# Parent  c822230fd22b6ce3e0475c211c9900049c9bd838# Parent  acb41098607aa17e4d1e9d1960752a2967b0d588
merge

diff -r c822230fd22b -r 5836854ca0a8 NEWS
--- a/NEWS	Mon Nov 25 20:25:22 2013 +0100
+++ b/NEWS	Tue Nov 26 15:54:03 2013 +0100
@@ -37,6 +37,8 @@
 * Elimination of fact duplicates:
     equals_zero_I ~> minus_unique
     diff_eq_0_iff_eq ~> right_minus_eq
+    nat_infinite ~> infinite_UNIV_nat
+    int_infinite ~> infinite_UNIV_int
 INCOMPATIBILITY.
 
 * Fact name consolidation:
diff -r c822230fd22b -r 5836854ca0a8 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Mon Nov 25 20:25:22 2013 +0100
+++ b/src/HOL/Library/Library.thy	Tue Nov 26 15:54:03 2013 +0100
@@ -65,6 +65,7 @@
   Transitive_Closure_Table
   Wfrec
   While_Combinator
+  Zorn
 begin
 end
 (*>*)
diff -r c822230fd22b -r 5836854ca0a8 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Mon Nov 25 20:25:22 2013 +0100
+++ b/src/Tools/subtyping.ML	Tue Nov 26 15:54:03 2013 +0100
@@ -129,7 +129,8 @@
 
 infixr ++> +@> (* lazy error msg composition *)
 
-fun err ++> prt = err #> apsnd (cons prt);
+fun (err : unit -> string * Pretty.T list) ++> (prt : Pretty.T) =
+  err #> apsnd (cons prt);
 val op +@> = Library.foldl op ++>;
 
 fun eval_err err = err ()