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 *)