removed obsolete expand_case_tac;

--- a/src/HOL/simpdata.ML	Wed Apr 26 14:19:13 2006 +0200
+++ b/src/HOL/simpdata.ML	Wed Apr 26 20:34:11 2006 +0200
@@ -410,13 +410,6 @@
 by (ALLGOALS (asm_simp_tac (HOL_ss addsimps prems)));
 qed "expand_case";
 
-(*Used in Auth proofs.  Typically P contains Vars that become instantiated
-  during unification.*)
-fun expand_case_tac P i =
-    res_inst_tac [("P",P)] expand_case i THEN
-    Simp_tac (i+1) THEN
-    Simp_tac i;
-
 (*This lemma restricts the effect of the rewrite rule u=v to the left-hand
   side of an equality.  Used in {Integ,Real}/simproc.ML*)
 Goal "x=y ==> (x=z) = (y=z)";