# HG changeset patch
# User nipkow
# Date 794664404 -3600
# Node ID d0320f916936de8fcbcd8d031329cba541954abf
# Parent  da0e86b4b352b722e454977972b0c85e4d74eec6
Enforced partial evaluation of mk_case_split_tac

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