moved split_tac

--- a/src/HOL/simpdata.ML	Wed Nov 27 17:00:25 1996 +0100
+++ b/src/HOL/simpdata.ML	Wed Nov 27 20:36:33 1996 +0100
@@ -262,6 +262,17 @@
                    "(if P then Q else R) = ((P-->Q) & (~P-->R))"
                    (fn _ => [rtac expand_if 1]);
 
+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;
+
+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;
+
+
 qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
   (fn _ => [split_tac [expand_if] 1, fast_tac HOL_cs 1]);
 
@@ -308,17 +319,6 @@
       addcongs [imp_cong];
 
 
-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;
-
-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;
-
-
 qed_goal "if_distrib" HOL.thy
   "f(if c then x else y) = (if c then f x else f y)" 
   (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);