--- 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
--- 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. *)