# HG changeset patch
# User paulson
# Date 841941768 -7200
# Node ID 6f20ecbd87cbbdb5f431fb54cf34c877d7f64764
# Parent  58b60b558e48a4bf6fe3153836580134e37f2aa0
Now uses thin_tac

diff -r 58b60b558e48 -r 6f20ecbd87cb src/HOL/IMP/Natural.ML
--- a/src/HOL/IMP/Natural.ML	Thu Sep 05 18:31:14 1996 +0200
+++ b/src/HOL/IMP/Natural.ML	Thu Sep 05 18:42:48 1996 +0200
@@ -18,6 +18,6 @@
 (* evaluation of com is deterministic *)
 goal Natural.thy "!!c s t. <c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
 by (etac evalc.induct 1);
-by (eres_inst_tac [("V", "<?c,s2> -c-> s1")] thin_rl 7);
+by (thin_tac "<?c,s2> -c-> s1" 7);
 by (ALLGOALS (deepen_tac evalc_cs 4));
 qed_spec_mp "com_det";