compile

--- a/src/HOL/ATP.thy	Wed Nov 16 17:06:14 2011 +0100
+++ b/src/HOL/ATP.thy	Wed Nov 16 17:19:08 2011 +0100
@@ -12,9 +12,9 @@
      "Tools/ATP/atp_util.ML"
      "Tools/ATP/atp_problem.ML"
      "Tools/ATP/atp_proof.ML"
-     "Tools/ATP/atp_systems.ML"
      ("Tools/ATP/atp_translate.ML")
      ("Tools/ATP/atp_reconstruct.ML")
+     ("Tools/ATP/atp_systems.ML")
 begin
 
 subsection {* Higher-order reasoning helpers *}
@@ -50,6 +50,7 @@
 
 use "Tools/ATP/atp_translate.ML"
 use "Tools/ATP/atp_reconstruct.ML"
+use "Tools/ATP/atp_systems.ML"
 
 setup ATP_Systems.setup
 

--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Nov 16 17:06:14 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Nov 16 17:19:08 2011 +0100
@@ -233,7 +233,7 @@
                       type_enc of
         [alias] => alias
       | _ => type_enc
-    val opts = [] |> type_enc <> Metis_Tactic.partial_typesN ? cons type_enc
+    val opts = [] |> type_enc <> partial_typesN ? cons type_enc
                   |> lam_trans <> metis_default_lam_trans ? cons lam_trans
   in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
 
@@ -1010,8 +1010,7 @@
          if member (op =) qs Show then "show" else "have")
     val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
     val reconstr =
-      Metis (if full_types then Metis_Tactic.full_typesN
-             else Metis_Tactic.partial_typesN, combinatorsN)
+      Metis (if full_types then full_typesN else partial_typesN, combinatorsN)
     fun do_facts (ls, ss) =
       reconstructor_command reconstr 1 1
           (ls |> sort_distinct (prod_ord string_ord int_ord),