src/HOL/simpdata.ML

--- a/src/HOL/simpdata.ML	Mon May 06 15:19:50 1996 +0200
+++ b/src/HOL/simpdata.ML	Mon May 06 15:21:05 1996 +0200
@@ -124,6 +124,11 @@
 fun split_tac splits = mktac (map mk_meta_eq splits)
 end;
 
+local val mktac = mk_case_split_inside_tac (meta_eq_to_obj_eq RS iffD2)
+in
+fun split_inside_tac splits = mktac (map mk_meta_eq splits)
+end;
+
 
 (* eliminiation of existential quantifiers in assumptions *)