src/FOL/simpdata.ML

--- a/src/FOL/simpdata.ML	Mon May 06 15:19:50 1996 +0200
+++ b/src/FOL/simpdata.ML	Mon May 06 15:21:05 1996 +0200
@@ -144,3 +144,10 @@
 in
 fun split_tac splits = mktac (map mk_meta_eq splits)
 end;
+
+local val mktac = mk_case_split_inside_tac meta_iffD
+in
+fun split_inside_tac splits = mktac (map mk_meta_eq splits)
+end;
+
+