# HG changeset patch
# User wenzelm
# Date 1321820887 -3600
# Node ID 13b101cee4257a6411693e581771419148913279
# Parent  16b4f5774621cb999f6823fedf39621a528be7cb
eliminated obsolete "standard";

diff -r 16b4f5774621 -r 13b101cee425 src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Sun Nov 20 21:07:10 2011 +0100
+++ b/src/HOL/Bali/WellForm.thy	Sun Nov 20 21:28:07 2011 +0100
@@ -733,13 +733,14 @@
  \<Longrightarrow> declclass m = Object"
 by (auto dest: class_Object simp add: methd_rec )
 
+lemmas iface_rec_induct' = iface_rec.induct [of "%x y z. P x y"] for P
+
 lemma wf_imethdsD: 
  "\<lbrakk>im \<in> imethds G I sig;wf_prog G; is_iface G I\<rbrakk> 
  \<Longrightarrow> \<not>is_static im \<and> accmodi im = Public"
 proof -
   assume asm: "wf_prog G" "is_iface G I" "im \<in> imethds G I sig"
 
-  note iface_rec_induct' = iface_rec.induct[of "(%x y z. P x y)", standard]  (* FIXME !? *)
   have "wf_prog G \<longrightarrow> 
          (\<forall> i im. iface G I = Some i \<longrightarrow> im \<in> imethds G I sig
                   \<longrightarrow> \<not>is_static im \<and> accmodi im = Public)" (is "?P G I")
diff -r 16b4f5774621 -r 13b101cee425 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sun Nov 20 21:07:10 2011 +0100
+++ b/src/HOL/Library/Multiset.thy	Sun Nov 20 21:28:07 2011 +0100
@@ -1527,7 +1527,7 @@
 apply (rule iffI)
  prefer 2
  apply blast
-apply (rule_tac A=A and f=f in fold_msetG_nonempty [THEN exE, standard])
+apply (rule_tac A1=A and f1=f in fold_msetG_nonempty [THEN exE])
 apply (blast intro: fold_msetG_determ)
 done
 
diff -r 16b4f5774621 -r 13b101cee425 src/ZF/Arith.thy
--- a/src/ZF/Arith.thy	Sun Nov 20 21:07:10 2011 +0100
+++ b/src/ZF/Arith.thy	Sun Nov 20 21:28:07 2011 +0100
@@ -88,7 +88,7 @@
 done
 
 (* [| 0 < k; k \<in> nat; !!j. [| j \<in> nat; k = succ(j) |] ==> Q |] ==> Q *)
-lemmas zero_lt_natE = zero_lt_lemma [THEN bexE, standard]
+lemmas zero_lt_natE = zero_lt_lemma [THEN bexE]
 
 
 subsection{*@{text natify}, the Coercion to @{term nat}*}