# HG changeset patch
# User blanchet
# Date 1286273059 -7200
# Node ID 1a908a35920b1269f57a8c74acfaec1f928536a9
# Parent  aa54f347e5e26fd78151d74d033268a35064147c
qualify names

diff -r aa54f347e5e2 -r 1a908a35920b src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Tue Oct 05 11:45:10 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Tue Oct 05 12:04:19 2010 +0200
@@ -230,7 +230,7 @@
 val optional_typed_helpers =
   [(["c_True", "c_False", "c_If"], @{thms True_or_False}),
    (["c_If"], @{thms if_True if_False})]
-val mandatory_helpers = @{thms fequal_def}
+val mandatory_helpers = @{thms Metis.fequal_def}
 
 val init_counters =
   [optional_helpers, optional_typed_helpers] |> maps (maps fst)
@@ -300,7 +300,7 @@
             let val ty_args = if full_types then [] else ty_args in
               if s = "equal" then
                 if top_level andalso length args = 2 then (name, [])
-                else (("c_fequal", @{const_name fequal}), ty_args)
+                else (("c_fequal", @{const_name Metis.fequal}), ty_args)
               else if top_level then
                 case s of
                   "c_False" => (("$false", s'), [])