compile
authorblanchet
Wed Nov 16 17:19:08 2011 +0100 (2011-11-16)
changeset 455223b951bbd2bee
parent 45521 0cd6e59bd0b5
child 45523 741f308c0f36
compile
src/HOL/ATP.thy
src/HOL/Tools/ATP/atp_reconstruct.ML
     1.1 --- a/src/HOL/ATP.thy	Wed Nov 16 17:06:14 2011 +0100
     1.2 +++ b/src/HOL/ATP.thy	Wed Nov 16 17:19:08 2011 +0100
     1.3 @@ -12,9 +12,9 @@
     1.4       "Tools/ATP/atp_util.ML"
     1.5       "Tools/ATP/atp_problem.ML"
     1.6       "Tools/ATP/atp_proof.ML"
     1.7 -     "Tools/ATP/atp_systems.ML"
     1.8       ("Tools/ATP/atp_translate.ML")
     1.9       ("Tools/ATP/atp_reconstruct.ML")
    1.10 +     ("Tools/ATP/atp_systems.ML")
    1.11  begin
    1.12  
    1.13  subsection {* Higher-order reasoning helpers *}
    1.14 @@ -50,6 +50,7 @@
    1.15  
    1.16  use "Tools/ATP/atp_translate.ML"
    1.17  use "Tools/ATP/atp_reconstruct.ML"
    1.18 +use "Tools/ATP/atp_systems.ML"
    1.19  
    1.20  setup ATP_Systems.setup
    1.21  
     2.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Nov 16 17:06:14 2011 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Nov 16 17:19:08 2011 +0100
     2.3 @@ -233,7 +233,7 @@
     2.4                        type_enc of
     2.5          [alias] => alias
     2.6        | _ => type_enc
     2.7 -    val opts = [] |> type_enc <> Metis_Tactic.partial_typesN ? cons type_enc
     2.8 +    val opts = [] |> type_enc <> partial_typesN ? cons type_enc
     2.9                    |> lam_trans <> metis_default_lam_trans ? cons lam_trans
    2.10    in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
    2.11  
    2.12 @@ -1010,8 +1010,7 @@
    2.13           if member (op =) qs Show then "show" else "have")
    2.14      val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
    2.15      val reconstr =
    2.16 -      Metis (if full_types then Metis_Tactic.full_typesN
    2.17 -             else Metis_Tactic.partial_typesN, combinatorsN)
    2.18 +      Metis (if full_types then full_typesN else partial_typesN, combinatorsN)
    2.19      fun do_facts (ls, ss) =
    2.20        reconstructor_command reconstr 1 1
    2.21            (ls |> sort_distinct (prod_ord string_ord int_ord),