# HG changeset patch
# User wenzelm
# Date 1146076451 -7200
# Node ID 896eb8056e97d4f45578d0eec1c9e11d48a5b8a0
# Parent  0fab37327f91db3a7a4f7bdd85520d0750e33b2b
removed obsolete expand_case_tac;

diff -r 0fab37327f91 -r 896eb8056e97 src/HOL/simpdata.ML
--- 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)";