--- a/src/FOL/FOL.thy Sat Nov 19 21:23:16 2011 +0100
+++ b/src/FOL/FOL.thy Sun Nov 20 13:29:12 2011 +0100
@@ -408,7 +408,7 @@
unfolding atomize_conj induct_conj_def .
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
-lemmas induct_rulify [symmetric, standard] = induct_atomize
+lemmas induct_rulify [symmetric] = induct_atomize
lemmas induct_rulify_fallback =
induct_forall_def induct_implies_def induct_equal_def induct_conj_def
--- a/src/FOLP/IFOLP.thy Sat Nov 19 21:23:16 2011 +0100
+++ b/src/FOLP/IFOLP.thy Sun Nov 20 13:29:12 2011 +0100
@@ -435,8 +435,11 @@
apply (erule sym)
done
-(*calling "standard" reduces maxidx to 0*)
-lemmas ssubst = sym [THEN subst, standard]
+schematic_lemma ssubst: "p:b=a \<Longrightarrow> q:P(a) \<Longrightarrow> ?p:P(b)"
+ apply (drule sym)
+ apply (erule subst)
+ apply assumption
+ done
(*A special case of ex1E that would otherwise need quantifier expansion*)
schematic_lemma ex1_equalsE: "[| p:EX! x. P(x); q:P(a); r:P(b) |] ==> ?d:a=b"