diff -r da0e86b4b352 -r d0320f916936 simpdata.ML --- a/simpdata.ML Wed Mar 01 17:44:05 1995 +0100 +++ b/simpdata.ML Wed Mar 08 13:06:44 1995 +0100 @@ -111,8 +111,10 @@ addsimps ([if_True, if_False, o_apply, conj_assoc] @ simp_thms) addcongs [imp_cong]; -fun split_tac splits = - mk_case_split_tac (meta_eq_to_obj_eq RS iffD2) (map mk_meta_eq splits); +local val mktac = mk_case_split_tac (meta_eq_to_obj_eq RS iffD2) +in +fun split_tac splits = mktac (map mk_meta_eq splits) +end; (* eliminiation of existential quantifiers in assumptions *)