diff -r 827730aea9e8 -r 27a8ad9612a3 src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -568,7 +568,7 @@
   (* Main function to start metis prove and reconstruction *)
   fun FOL_SOLVE mode ctxt cls ths0 =
     let val thy = ProofContext.theory_of ctxt
-        val th_cls_pairs = map (fn th => (PureThy.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
+        val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
         val ths = List.concat (map #2 th_cls_pairs)
         val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause"
                 else ();