diff -r 5c31d06ead04 -r 64c9f2364dae src/HOL/Isar_examples/KnasterTarski.thy
--- a/src/HOL/Isar_examples/KnasterTarski.thy	Fri Jul 30 13:43:26 1999 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy	Fri Jul 30 13:44:29 1999 +0200
@@ -25,7 +25,7 @@
 
   assume mono: "mono f";
   show "f ??a = ??a";
-  proof same;
+  proof -;
     {{;
       fix x;
       assume mem: "x : ??H";