# HG changeset patch
# User blanchet
# Date 1284539169 -7200
# Node ID 76603e40bd4cf490979d802b26623b0502eeda9b
# Parent  9e544eb396dcc57f0ca771bd86ee2e813ae1c485
in debug mode, don't touch "$true" and "$false"

diff -r 9e544eb396dc -r 76603e40bd4c src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Sep 14 23:38:36 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Sep 15 10:26:09 2010 +0200
@@ -126,7 +126,9 @@
 
 fun nice_name (full_name, _) NONE = (full_name, NONE)
   | nice_name (full_name, desired_name) (SOME the_pool) =
-    case Symtab.lookup (fst the_pool) full_name of
+    if String.isPrefix "$" full_name then
+      (full_name, SOME the_pool)
+    else case Symtab.lookup (fst the_pool) full_name of
       SOME nice_name => (nice_name, SOME the_pool)
     | NONE =>
       let