# HG changeset patch
# User blanchet
# Date 1321460348 -3600
# Node ID 3b951bbd2beecb7aec82c65678f1318692388056
# Parent  0cd6e59bd0b5fd7069877ae3f65abe56f4c2b7cc
compile

diff -r 0cd6e59bd0b5 -r 3b951bbd2bee src/HOL/ATP.thy
--- 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
 
diff -r 0cd6e59bd0b5 -r 3b951bbd2bee src/HOL/Tools/ATP/atp_reconstruct.ML
--- 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),