--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Fri Jul 24 13:44:27 1998 +0200
@@ -878,9 +878,9 @@
\ --> seq_take n`(x @@ (t>>y1)) = seq_take n`(x @@ (t>>y2)))";
by (Seq_induct_tac "x" [] 1);
by (strip_tac 1);
-by (res_inst_tac [("n","n")] natE 1);
+by (exhaust_tac "n" 1);
by Auto_tac;
-by (res_inst_tac [("n","n")] natE 1);
+by (exhaust_tac "n" 1);
by Auto_tac;
qed"take_reduction1";
@@ -900,9 +900,9 @@
\ --> seq_take n`(x @@ (t>>y1)) << seq_take n`(x @@ (t>>y2)))";
by (Seq_induct_tac "x" [] 1);
by (strip_tac 1);
-by (res_inst_tac [("n","n")] natE 1);
+by (exhaust_tac "n" 1);
by Auto_tac;
-by (res_inst_tac [("n","n")] natE 1);
+by (exhaust_tac "n" 1);
by Auto_tac;
qed"take_reduction_less1";