# HG changeset patch
# User wenzelm
# Date 938727442 -7200
# Node ID a410fa2d0a161d3940d79b54c9ad1024cfb7dedc
# Parent  e302e4269087fd064b7b43168a49a168d8d10f0f
fixed 'is' match;

diff -r e302e4269087 -r a410fa2d0a16 src/HOL/Isar_examples/W_correct.thy
--- a/src/HOL/Isar_examples/W_correct.thy	Thu Sep 30 23:33:41 1999 +0200
+++ b/src/HOL/Isar_examples/W_correct.thy	Thu Sep 30 23:37:22 1999 +0200
@@ -82,9 +82,7 @@
 theorem W_correct: "W e a n = Ok (s, t, m) ==> $ s a |- e :: t";
 proof -;
   assume W_ok: "W e a n = Ok (s, t, m)";
-  let ?P = "%e. ALL a s t m n . Ok (s, t, m) = W e a n --> $ s a |- e :: t";
-    (* FIXME (is ...) fails!? *)
-  have "?P e";
+  have "ALL a s t m n . Ok (s, t, m) = W e a n --> $ s a |- e :: t" (is "?P e");
   proof (induct e);
     fix n; show "?P (Var n)"; by simp;
   next;