src/HOL/IMPP/Com.ML

--- a/src/HOL/IMPP/Com.ML	Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/Com.ML	Sat Sep 17 20:14:30 2005 +0200
@@ -1,3 +1,5 @@
+(* $Id$ *)
+
 val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl];
 
 Goalw [body_def] "finite (dom body)";
@@ -9,9 +11,4 @@
 by (Fast_tac 1);
 qed "WT_bodiesD";
 
-val WTs_elim_cases = map WTs.mk_cases
-   ["WT SKIP", "WT (X:==a)", "WT (LOCAL Y:=a IN c)", 
-    "WT (c1;;c2)","WT (IF b THEN c1 ELSE c2)", "WT (WHILE b DO c)",
-    "WT (BODY P)", "WT (X:=CALL P(a))"];
-
 AddSEs WTs_elim_cases;