author | blanchet |
Wed, 15 Sep 2010 10:26:09 +0200 | |
changeset 39384 | 76603e40bd4c |
parent 39377 | 9e544eb396dc |
child 39385 | 0049301f7333 |
--- 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