src/FOL/simpdata.ML

--- a/src/FOL/simpdata.ML	Fri Nov 07 18:02:15 1997 +0100
+++ b/src/FOL/simpdata.ML	Fri Nov 07 18:05:25 1997 +0100
@@ -183,6 +183,8 @@
 fun split_inside_tac splits = mktac (map mk_meta_eq splits)
 end;
 
+val split_prem_tac = mk_case_split_prem_tac split_tac disjE conjE exE contrapos
+					    contrapos2 notnotD;
 
 (*** Standard simpsets ***)