# HG changeset patch
# User huffman
# Date 1315087791 25200
# Node ID a9635943a3e969539d5fdfbaddbb16f18eaad54d
# Parent  67b78d5dea5b231807652147327bd6a25d3bb6f3# Parent  ccfc7c193d2b998079e8a0e643662ef6d7d3ca48
merged

diff -r 67b78d5dea5b -r a9635943a3e9 src/HOL/Import/HOL4Compat.thy
--- a/src/HOL/Import/HOL4Compat.thy	Sat Sep 03 23:38:06 2011 +0200
+++ b/src/HOL/Import/HOL4Compat.thy	Sat Sep 03 15:09:51 2011 -0700
@@ -421,16 +421,6 @@
   assume allx': "ALL x. P x \<longrightarrow> x < z"
   have "EX s. ALL y. (EX x : Collect P. y < x) = (y < s)"
   proof (rule posreal_complete)
-    show "ALL x : Collect P. 0 < x"
-    proof safe
-      fix x
-      assume P: "P x"
-      from allx
-      have "P x \<longrightarrow> 0 < x"
-        ..
-      with P show "0 < x" by simp
-    qed
-  next
     from px
     show "EX x. x : Collect P"
       by auto
diff -r 67b78d5dea5b -r a9635943a3e9 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sat Sep 03 23:38:06 2011 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Sep 03 15:09:51 2011 -0700
@@ -1205,7 +1205,7 @@
     val ind_prems' =
       map (fn (_, f as Free (_, T)) => list_all_free ([("x", fsT')],
         HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
-          (List.last (binder_types T) --> HOLogic.boolT) -->
+          Term.range_type T -->
             HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
       maps (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
         map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $
diff -r 67b78d5dea5b -r a9635943a3e9 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Sat Sep 03 23:38:06 2011 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Sat Sep 03 15:09:51 2011 -0700
@@ -303,7 +303,7 @@
               vs HOLogic.unit;
             val s' = list_abs (ps,
               Const ("Nominal.supp", fastype_of1 (Ts, s) -->
-                List.last (binder_types T) --> HOLogic.boolT) $ s);
+                Term.range_type T) $ s);
             val supports_rule' = Thm.lift_rule goal supports_rule;
             val _ $ (_ $ S $ _) =
               Logic.strip_assums_concl (hd (prems_of supports_rule'));
diff -r 67b78d5dea5b -r a9635943a3e9 src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Sat Sep 03 23:38:06 2011 +0200
+++ b/src/HOL/RComplete.thy	Sat Sep 03 15:09:51 2011 -0700
@@ -33,8 +33,8 @@
 text {* Only used in HOL/Import/HOL4Compat.thy; delete? *}
 
 lemma posreal_complete:
-  assumes positive_P: "\<forall>x \<in> P. (0::real) < x"
-    and not_empty_P: "\<exists>x. x \<in> P"
+  fixes P :: "real set"
+  assumes not_empty_P: "\<exists>x. x \<in> P"
     and upper_bound_Ex: "\<exists>y. \<forall>x \<in> P. x<y"
   shows "\<exists>S. \<forall>y. (\<exists>x \<in> P. y < x) = (y < S)"
 proof -