# HG changeset patch
# User blanchet
# Date 1284540322 -7200
# Node ID fcbb3bb3ebe2b2ac9e1946cd1b666553678372ad
# Parent  0049301f7333027d235abcef53eb9ba6fcf1384e# Parent  ddfafa97da2f36b008a189bc80c90ecf15c68b44
merge

diff -r ddfafa97da2f -r fcbb3bb3ebe2 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Wed Sep 15 09:36:39 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Sep 15 10:45:22 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
diff -r ddfafa97da2f -r fcbb3bb3ebe2 src/Tools/Metis/metis.ML
--- a/src/Tools/Metis/metis.ML	Wed Sep 15 09:36:39 2010 +0200
+++ b/src/Tools/Metis/metis.ML	Wed Sep 15 10:45:22 2010 +0200
@@ -179,7 +179,7 @@
 (* Pointer equality using the run-time system.                               *)
 (* ------------------------------------------------------------------------- *)
 
-fun pointerEqual (x : 'a, y : 'a) = PolyML.pointerEq(x,y);
+fun pointerEqual (x : 'a, y : 'a) = pointer_eq (x, y) (* MODIFIED by Jasmin Blanchette *)
 
 (* ------------------------------------------------------------------------- *)
 (* Timing function applications.                                             *)