--- 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