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;