# HG changeset patch
# User blanchet
# Date 1268916230 -3600
# Node ID d4c4f88f643289c1e24fa69491b030a9c91c4922
# Parent  c5f54c04a1aabc48d2ac7fc470e8a8be3218802a
fix Mirabelle after renaming Sledgehammer structures

diff -r c5f54c04a1aa -r d4c4f88f6432 src/HOL/Mirabelle/Tools/mirabelle_metis.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Thu Mar 18 13:14:54 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Thu Mar 18 13:43:50 2010 +0100
@@ -18,7 +18,7 @@
 
     val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
 
-    fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
+    fun metis ctxt = Metis_Tactics.metis_tac ctxt (thms @ facts)
   in
     (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
     |> prefix (metis_tag id)
diff -r c5f54c04a1aa -r d4c4f88f6432 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Mar 18 13:14:54 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Mar 18 13:43:50 2010 +0100
@@ -325,7 +325,7 @@
     if success then (message, SH_OK (time_isa, time_atp, theorem_names))
     else (message, SH_FAIL(time_isa, time_atp))
   end
-  handle Res_HOL_Clause.TOO_TRIVIAL => ("trivial", SH_OK (0, 0, []))
+  handle Sledgehammer_HOL_Clause.TOO_TRIVIAL => ("trivial", SH_OK (0, 0, []))
        | ERROR msg => ("error: " ^ msg, SH_ERROR)
        | TimeLimit.TimeOut => ("timeout", SH_ERROR)
 
@@ -407,8 +407,8 @@
     ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
   let
     fun metis thms ctxt =
-      if full then MetisTools.metisFT_tac ctxt thms
-      else MetisTools.metis_tac ctxt thms
+      if full then Metis_Tactics.metisFT_tac ctxt thms
+      else Metis_Tactics.metis_tac ctxt thms
     fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
 
     fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"