# HG changeset patch
# User wenzelm
# Date 1217883300 -7200
# Node ID dcec1c564f05a1084330056b4dfc9f9f5d415789
# Parent  d3d7038fb7b575d1de5c7b18baf957b4a35b5b68
meta_subst: xsymbols make it work with clean Pure;

diff -r d3d7038fb7b5 -r dcec1c564f05 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 **)