# HG changeset patch
# User wenzelm
# Date 1321792152 -3600
# Node ID d320f2f9f331651fd377e2343fcf2effbc0148af
# Parent  7247ade03aa9fba75cef63ec1e52ffd0d94370c0
tuned;

diff -r 7247ade03aa9 -r d320f2f9f331 src/FOL/FOL.thy
--- 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
 
diff -r 7247ade03aa9 -r d320f2f9f331 src/FOLP/IFOLP.thy
--- 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"