IOA/meta_theory/IOA.ML

--- a/IOA/meta_theory/IOA.ML	Tue Mar 14 09:42:49 1995 +0100
+++ b/IOA/meta_theory/IOA.ML	Tue Mar 14 09:43:12 1995 +0100
@@ -45,7 +45,7 @@
 qed "mk_behaviour_thm";
 
 goalw IOA.thy [reachable_def] "!!A. s:starts_of(A) ==> reachable(A,s)";
-  by (res_inst_tac [("x","<(%i.None),(%i.s)>::('action,'a)execution")] bexI 1);
+  by (res_inst_tac [("x","<%i.None,%i.s>")] bexI 1);
   by (simp_tac SS 1);
   by (asm_simp_tac (SS addsimps exec_rws) 1);
 qed "reachable_0";
@@ -80,8 +80,7 @@
   by (nat_ind_tac "n" 1);
   by (fast_tac (set_cs addIs [p1,reachable_0]) 1);
   by (eres_inst_tac[("x","n1")]allE 1);
-  by (eres_inst_tac[("P","%x.!a::'action.?Q(x,a)"),
-                    ("opt","fst(ex,n1)")] optE 1);
+  by (eres_inst_tac[("P","%x.!a.?Q(x,a)"), ("opt","fst(ex,n1)")] optE 1);
   by (asm_simp_tac HOL_ss 1);
   by (safe_tac HOL_cs);
   by (etac (p2 RS mp) 1);