# HG changeset patch
# User nipkow
# Date 794663805 -3600
# Node ID f8a202891ac92775273a8d13a620aeba67ae4410
# Parent  bd9ab32bfa304a05101111e94c55387b8a94c926
Enforced partial evaluation of mk_case_split_tac

diff -r bd9ab32bfa30 -r f8a202891ac9 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Mar 08 12:37:59 1995 +0100
+++ b/src/HOL/simpdata.ML	Wed Mar 08 12:56:45 1995 +0100
@@ -111,8 +111,11 @@
       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 *)