# HG changeset patch
# User nipkow
# Date 794667668 -3600
# Node ID d9edeb96b51ccb4fb7997a00adadbfdfc8784aeb
# Parent  f8a202891ac92775273a8d13a620aeba67ae4410
Enforced partial evaluation of mk_case_split_tac.

diff -r f8a202891ac9 -r d9edeb96b51c src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Wed Mar 08 12:56:45 1995 +0100
+++ b/src/FOL/simpdata.ML	Wed Mar 08 14:01:08 1995 +0100
@@ -130,5 +130,7 @@
 qed_goal "meta_iffD" FOL.thy "[| P==Q; Q |] ==> P"
         (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]);
 
-fun split_tac splits =
-    mk_case_split_tac meta_iffD (map mk_meta_eq splits);
+local val mktac = mk_case_split_tac meta_iffD
+in
+fun split_tac splits = mktac (map mk_meta_eq splits)
+end;