src/HOL/Library/Eval_Witness.thy

--- a/src/HOL/Library/Eval_Witness.thy	Fri Feb 22 12:01:57 2008 +0100
+++ b/src/HOL/Library/Eval_Witness.thy	Fri Feb 22 16:31:37 2008 +0100
@@ -86,9 +86,9 @@
   naturals, since ML integers are different.
 *}
 
-lemma "\<exists>n::nat. n = 1"
-apply (eval_witness "Isabelle_Eval.Suc Isabelle_Eval.Zero_nat")
-done
+(*lemma "\<exists>n::nat. n = 1"
+apply (eval_witness "Suc Zero_nat")
+done*)
 
 text {* 
   Since polymorphism is not allowed, we must specify the