1.1 --- a/src/HOL/Import/HOL4Compat.thy	Sat Sep 03 23:38:06 2011 +0200
     1.2 +++ b/src/HOL/Import/HOL4Compat.thy	Sat Sep 03 15:09:51 2011 -0700
     1.3 @@ -421,16 +421,6 @@
     1.4    assume allx': "ALL x. P x \<longrightarrow> x < z"
     1.5    have "EX s. ALL y. (EX x : Collect P. y < x) = (y < s)"
     1.6    proof (rule posreal_complete)
     1.7 -    show "ALL x : Collect P. 0 < x"
     1.8 -    proof safe
     1.9 -      fix x
    1.10 -      assume P: "P x"
    1.11 -      from allx
    1.12 -      have "P x \<longrightarrow> 0 < x"
    1.13 -        ..
    1.14 -      with P show "0 < x" by simp
    1.15 -    qed
    1.16 -  next
    1.17      from px
    1.18      show "EX x. x : Collect P"
    1.19        by auto

     2.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat Sep 03 23:38:06 2011 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Sep 03 15:09:51 2011 -0700
     2.3 @@ -1205,7 +1205,7 @@
     2.4      val ind_prems' =
     2.5        map (fn (_, f as Free (_, T)) => list_all_free ([("x", fsT')],
     2.6          HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
     2.7 -          (List.last (binder_types T) --> HOLogic.boolT) -->
     2.8 +          Term.range_type T -->
     2.9              HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
    2.10        maps (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
    2.11          map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $

     3.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Sat Sep 03 23:38:06 2011 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Sat Sep 03 15:09:51 2011 -0700
     3.3 @@ -303,7 +303,7 @@
     3.4                vs HOLogic.unit;
     3.5              val s' = list_abs (ps,
     3.6                Const ("Nominal.supp", fastype_of1 (Ts, s) -->
     3.7 -                List.last (binder_types T) --> HOLogic.boolT) $ s);
     3.8 +                Term.range_type T) $ s);
     3.9              val supports_rule' = Thm.lift_rule goal supports_rule;
    3.10              val _ $ (_ $ S $ _) =
    3.11                Logic.strip_assums_concl (hd (prems_of supports_rule'));

     4.1 --- a/src/HOL/RComplete.thy	Sat Sep 03 23:38:06 2011 +0200
     4.2 +++ b/src/HOL/RComplete.thy	Sat Sep 03 15:09:51 2011 -0700
     4.3 @@ -33,8 +33,8 @@
     4.4  text {* Only used in HOL/Import/HOL4Compat.thy; delete? *}
     4.5  
     4.6  lemma posreal_complete:
     4.7 -  assumes positive_P: "\<forall>x \<in> P. (0::real) < x"
     4.8 -    and not_empty_P: "\<exists>x. x \<in> P"
     4.9 +  fixes P :: "real set"
    4.10 +  assumes not_empty_P: "\<exists>x. x \<in> P"
    4.11      and upper_bound_Ex: "\<exists>y. \<forall>x \<in> P. x<y"
    4.12    shows "\<exists>S. \<forall>y. (\<exists>x \<in> P. y < x) = (y < S)"
    4.13  proof -