Adapted to changes in FixedPoint theory.

--- a/src/HOL/Hilbert_Choice.thy	Fri Oct 13 18:14:12 2006 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Fri Oct 13 18:15:18 2006 +0200
@@ -419,7 +419,7 @@
 lemma GreatestM_nat_le:
   "P x ==> \<forall>y. P y --> m y < b
     ==> (m x::nat) <= m (GreatestM m P)"
-  apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec])
+  apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec, of P])
   done
 
 

--- a/src/HOL/Hyperreal/Transcendental.thy	Fri Oct 13 18:14:12 2006 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Fri Oct 13 18:15:18 2006 +0200
@@ -1942,7 +1942,7 @@
 
 lemma real_root_eq_iff [simp]:
      "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x = root(Suc n) y) = (x = y)"
-apply (auto intro!: order_antisym)
+apply (auto intro!: order_antisym [where 'a = real])
 apply (rule_tac n1 = n in real_root_le_iff [THEN iffD1])
 apply (rule_tac [4] n1 = n in real_root_le_iff [THEN iffD1], auto)
 done

--- a/src/HOL/IMP/Denotation.thy	Fri Oct 13 18:14:12 2006 +0200
+++ b/src/HOL/IMP/Denotation.thy	Fri Oct 13 18:15:18 2006 +0200
@@ -62,7 +62,7 @@
 apply fast
 
 (* while *)
-apply (erule lfp_induct [OF _ Gamma_mono])
+apply (erule lfp_induct_set [OF _ Gamma_mono])
 apply (unfold Gamma_def)
 apply fast
 done

--- a/src/HOL/NanoJava/Example.thy	Fri Oct 13 18:14:12 2006 +0200
+++ b/src/HOL/NanoJava/Example.thy	Fri Oct 13 18:15:18 2006 +0200
@@ -92,17 +92,17 @@
         "s:x\<ge>Suc n = (\<exists>a. x=Addr a \<and> heap s a \<noteq> None \<and> s:get_field s a pred\<ge>n)"
 
 lemma Nat_atleast_lupd [rule_format, simp]: 
- "\<forall>s v. lupd(x\<mapsto>y) s:v \<ge> n = (s:v \<ge> n)"
+ "\<forall>s v::val. lupd(x\<mapsto>y) s:v \<ge> n = (s:v \<ge> n)"
 apply (induct n)
 by  auto
 
 lemma Nat_atleast_set_locs [rule_format, simp]: 
- "\<forall>s v. set_locs l s:v \<ge> n = (s:v \<ge> n)"
+ "\<forall>s v::val. set_locs l s:v \<ge> n = (s:v \<ge> n)"
 apply (induct n)
 by auto
 
 lemma Nat_atleast_del_locs [rule_format, simp]: 
- "\<forall>s v. del_locs s:v \<ge> n = (s:v \<ge> n)"
+ "\<forall>s v::val. del_locs s:v \<ge> n = (s:v \<ge> n)"
 apply (induct n)
 by auto
 
@@ -121,7 +121,7 @@
 by auto
 
 lemma Nat_atleast_newC [rule_format]: 
-  "heap s aa = None \<Longrightarrow> \<forall>v. s:v \<ge> n \<longrightarrow> hupd(aa\<mapsto>obj) s:v \<ge> n"
+  "heap s aa = None \<Longrightarrow> \<forall>v::val. s:v \<ge> n \<longrightarrow> hupd(aa\<mapsto>obj) s:v \<ge> n"
 apply (induct n)
 apply  auto
 apply  (case_tac "aa=a")

--- a/src/HOL/TLA/Intensional.thy	Fri Oct 13 18:14:12 2006 +0200
+++ b/src/HOL/TLA/Intensional.thy	Fri Oct 13 18:15:18 2006 +0200
@@ -180,7 +180,7 @@
   Valid_def:   "|- A    ==  ALL w. w |= A"
 
   unl_con:     "LIFT #c w  ==  c"
-  unl_lift:    "LIFT f<x> w == f (x w)"
+  unl_lift:    "lift f x w == f (x w)"
   unl_lift2:   "LIFT f<x, y> w == f (x w) (y w)"
   unl_lift3:   "LIFT f<x, y, z> w == f (x w) (y w) (z w)"