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