1.1 --- a/NEWS	Mon Nov 25 20:25:22 2013 +0100
     1.2 +++ b/NEWS	Tue Nov 26 15:54:03 2013 +0100
     1.3 @@ -37,6 +37,8 @@
     1.4  * Elimination of fact duplicates:
     1.5      equals_zero_I ~> minus_unique
     1.6      diff_eq_0_iff_eq ~> right_minus_eq
     1.7 +    nat_infinite ~> infinite_UNIV_nat
     1.8 +    int_infinite ~> infinite_UNIV_int
     1.9  INCOMPATIBILITY.
    1.10  
    1.11  * Fact name consolidation:

     2.1 --- a/src/HOL/Library/Library.thy	Mon Nov 25 20:25:22 2013 +0100
     2.2 +++ b/src/HOL/Library/Library.thy	Tue Nov 26 15:54:03 2013 +0100
     2.3 @@ -65,6 +65,7 @@
     2.4    Transitive_Closure_Table
     2.5    Wfrec
     2.6    While_Combinator
     2.7 +  Zorn
     2.8  begin
     2.9  end
    2.10  (*>*)

     3.1 --- a/src/Tools/subtyping.ML	Mon Nov 25 20:25:22 2013 +0100
     3.2 +++ b/src/Tools/subtyping.ML	Tue Nov 26 15:54:03 2013 +0100
     3.3 @@ -129,7 +129,8 @@
     3.4  
     3.5  infixr ++> +@> (* lazy error msg composition *)
     3.6  
     3.7 -fun err ++> prt = err #> apsnd (cons prt);
     3.8 +fun (err : unit -> string * Pretty.T list) ++> (prt : Pretty.T) =
     3.9 +  err #> apsnd (cons prt);
    3.10  val op +@> = Library.foldl op ++>;
    3.11  
    3.12  fun eval_err err = err ()