# HG changeset patch
# User paulson
# Date 864306605 -7200
# Node ID 078d5f7d0d09eef9b22f8a0835170a8bc39b55d2
# Parent  2ee6c397003dd19310f57186d349a76dbc6630c4
Uses option_case_tac

diff -r 2ee6c397003d -r 078d5f7d0d09 src/HOL/IOA/IOA.ML
--- a/src/HOL/IOA/IOA.ML	Thu May 22 15:09:37 1997 +0200
+++ b/src/HOL/IOA/IOA.ML	Thu May 22 15:10:05 1997 +0200
@@ -82,12 +82,10 @@
   by (nat_ind_tac "n" 1);
   by (fast_tac (!claset addIs [p1,reachable_0]) 1);
   by (eres_inst_tac[("x","n")]allE 1);
-  by (eres_inst_tac[("P","%x.!a.?Q x a"), ("opt","fst ex n")] optionE 1);
-  by (Asm_simp_tac 1);
+  by (option_case_tac "fst ex n" 1);
   by (safe_tac (!claset));
   by (etac (p2 RS mp) 1);
-  by (ALLGOALS(fast_tac(!claset addDs [hd Option.option.inject RS iffD1,
-                                      reachable_n])));
+  by (ALLGOALS(fast_tac(!claset addDs [reachable_n])));
 qed "invariantI";
 
 val [p1,p2] = goal IOA.thy