src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Wed Sep 29 10:05:44 2010 +0200
+++ b/src/HOL/HOL.thy	Wed Sep 29 11:02:24 2010 +0200
@@ -834,8 +834,6 @@
   val subst = @{thm subst}
   val sym = @{thm sym}
   val thin_refl = @{thm thin_refl};
-  val prop_subst = @{lemma "PROP P t ==> PROP prop (x = t ==> PROP P x)"
-                     by (unfold prop_def) (drule eq_reflection, unfold)}
 end);
 open Hypsubst;