src/Provers/hypsubst.ML

--- a/src/Provers/hypsubst.ML	Mon Aug 04 21:24:19 2008 +0200
+++ b/src/Provers/hypsubst.ML	Mon Aug 04 22:55:00 2008 +0200
@@ -62,7 +62,7 @@
 
 exception EQ_VAR;
 
-val meta_subst = @{lemma "PROP P t ==> PROP prop (x == t ==> PROP P x)"
+val meta_subst = @{lemma "PROP P t \<Longrightarrow> PROP prop (x \<equiv> t \<Longrightarrow> PROP P x)"
   by (unfold prop_def)}
 
 (** Simple version: Just subtitute one hypothesis, specified by index k **)