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"