diff -r be01ba66ba7b -r e0d0e5b4994f simpdata.ML
--- 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 *)