--- a/simpdata.ML Tue Aug 02 16:43:39 1994 +0200
+++ b/simpdata.ML Wed Aug 03 11:00:40 1994 +0200
@@ -65,7 +65,7 @@
in
-val meta_obj_reflection = prove_goal HOL.thy "x==y ==> x=y"
+val meta_eq_to_obj_eq = prove_goal HOL.thy "x==y ==> x=y"
(fn [prem] => [rewtac prem, rtac refl 1]);
val eq_sym_conv = prover "(x=y) = (y=x)";
@@ -106,7 +106,7 @@
addcongs [imp_cong];
fun split_tac splits =
- mk_case_split_tac (meta_obj_reflection RS iffD2) (map mk_eq splits);
+ mk_case_split_tac (meta_eq_to_obj_eq RS iffD2) (map mk_eq splits);
(* eliminiation of existential quantifiers in assumptions *)