# HG changeset patch
# User lcp
# Date 799500909 -7200
# Node ID fc4fb6e8a6368476d19dba3ec54aed50f7e1b537
# Parent  c1ccf6679a96ca4e47ad4d8aa3ae19a26a6fb6b1
Imported meta_eq_to_obj_eq from HOL for use with 'split'.

diff -r c1ccf6679a96 -r fc4fb6e8a636 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Wed May 03 12:22:17 1995 +0200
+++ b/src/FOL/simpdata.ML	Wed May 03 13:35:09 1995 +0200
@@ -131,9 +131,13 @@
 
 val FOL_ss = IFOL_ss addsimps cla_rews;
 
+(*Used in ZF, perhaps elsewhere?*)
+val meta_eq_to_obj_eq = prove_goal IFOL.thy "x==y ==> x=y"
+  (fn [prem] => [rewtac prem, rtac refl 1]);
+
 (*** case splitting ***)
 
-qed_goal "meta_iffD" FOL.thy "[| P==Q; Q |] ==> P"
+qed_goal "meta_iffD" IFOL.thy "[| P==Q; Q |] ==> P"
         (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]);
 
 local val mktac = mk_case_split_tac meta_iffD