diff -r f1c76cf10915 -r e8664643f543 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Fri Oct 24 10:41:15 2008 +0200
+++ b/src/FOL/IFOL.thy	Fri Oct 24 17:48:33 2008 +0200
@@ -101,6 +101,7 @@
   (* Equality *)
 
   refl:         "a=a"
+  subst:        "a=b \<Longrightarrow> P(a) \<Longrightarrow> P(b)"
 
   (* Propositional logic *)
 
@@ -125,7 +126,10 @@
   exI:          "P(x) ==> (EX x. P(x))"
   exE:          "[| EX x. P(x);  !!x. P(x) ==> R |] ==> R"
 
-  (* Reflection *)
+
+axioms
+
+  (* Reflection, admissible *)
 
   eq_reflection:  "(x=y)   ==> (x==y)"
   iff_reflection: "(P<->Q) ==> (P==Q)"
@@ -134,18 +138,6 @@
 lemmas strip = impI allI
 
 
-text{*Thanks to Stephan Merz*}
-theorem subst:
-  assumes eq: "a = b" and p: "P(a)"
-  shows "P(b)"
-proof -
-  from eq have meta: "a \<equiv> b"
-    by (rule eq_reflection)
-  from p show ?thesis
-    by (unfold meta)
-qed
-
-
 defs
   (* Definitions *)