# HG changeset patch
# User berghofe
# Date 1210150595 -7200
# Node ID e36a92ff543e291a9909d61841a275092f5ec055
# Parent  f2d75fd231249f81698d7acc0afa7cc063980c78
Instantiated some rules to avoid problems with HO unification.

diff -r f2d75fd23124 -r e36a92ff543e src/HOL/Induct/LList.thy
--- a/src/HOL/Induct/LList.thy	Wed May 07 10:56:34 2008 +0200
+++ b/src/HOL/Induct/LList.thy	Wed May 07 10:56:35 2008 +0200
@@ -566,7 +566,7 @@
 apply (drule imageI)
 apply (erule LList_equalityI, safe)
 apply (erule llist.cases, simp_all)
-apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I])+
+apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I, of _ _ _ f])+
 apply assumption  
 done
 
@@ -574,7 +574,7 @@
 apply (drule imageI)
 apply (erule LList_equalityI, safe)
 apply (erule llist.cases, simp_all)
-apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I])+
+apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I, of _ _ _ "%x. x"])+
 apply assumption 
 done
 
diff -r f2d75fd23124 -r e36a92ff543e src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Wed May 07 10:56:34 2008 +0200
+++ b/src/HOL/Inductive.thy	Wed May 07 10:56:35 2008 +0200
@@ -112,8 +112,8 @@
   and P_f: "!!S. P S ==> P(f S)"
   and P_Union: "!!M. !S:M. P S ==> P(Union M)"
   shows "P(lfp f)"
-  using assms unfolding Sup_set_def [symmetric]
-  by (rule lfp_ordinal_induct) 
+  using assms unfolding Sup_set_eq [symmetric]
+  by (rule lfp_ordinal_induct [where P=P])
 
 
 text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct}, 
@@ -215,7 +215,7 @@
 apply (rule Un_least [THEN Un_least])
 apply (rule subset_refl, assumption)
 apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
-apply (rule monoD, assumption)
+apply (rule monoD [where f=f], assumption)
 apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
 done
 
diff -r f2d75fd23124 -r e36a92ff543e src/HOL/NumberTheory/EulerFermat.thy
--- a/src/HOL/NumberTheory/EulerFermat.thy	Wed May 07 10:56:34 2008 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.thy	Wed May 07 10:56:35 2008 +0200
@@ -162,7 +162,7 @@
 lemma RRset_gcd [rule_format]:
     "is_RRset A m ==> a \<in> A --> zgcd (a, m) = 1"
   apply (unfold is_RRset_def)
-  apply (rule RsetR.induct, auto)
+  apply (rule RsetR.induct [where P="%A. a \<in> A --> zgcd (a, m) = 1"], auto)
   done
 
 lemma RsetR_zmult_mono:
@@ -219,7 +219,7 @@
   "1 < m ==>
     is_RRset A m ==> [a = b] (mod m) ==> a \<in> A --> b \<in> A --> a = b"
   apply (unfold is_RRset_def)
-  apply (rule RsetR.induct)
+  apply (rule RsetR.induct [where P="%A. a \<in> A --> b \<in> A --> a = b"])
     apply (auto simp add: zcong_sym)
   done