diff -r 7fb79905ed72 -r aa54f347e5e2 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Oct 05 11:14:56 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Oct 05 11:45:10 2010 +0200
@@ -532,7 +532,7 @@
 
 fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s)
 fun is_isabelle_literal_genuine t =
-  case t of _ $ (Const (@{const_name skolem}, _) $ _) => false | _ => true
+  case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true
 
 fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0