src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 42579 2552c09b1a72
parent 42570 77f94ac04f32
child 42587 4fbb1de05169
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:25 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:25 2011 +0200
     1.3 @@ -45,6 +45,7 @@
     1.4  
     1.5  open ATP_Problem
     1.6  open ATP_Proof
     1.7 +open ATP_Systems
     1.8  open Metis_Translate
     1.9  open Sledgehammer_Util
    1.10  open Sledgehammer_Filter
    1.11 @@ -193,7 +194,7 @@
    1.12    | using_labels ls =
    1.13      "using " ^ space_implode " " (map string_for_label ls) ^ " "
    1.14  fun metis_name type_sys =
    1.15 -  if type_system_types_dangerous_types type_sys then "metisFT" else "metis"
    1.16 +  if level_of_type_sys type_sys = Unsound then "metis" else "metisFT"
    1.17  fun metis_call type_sys ss = command_call (metis_name type_sys) ss
    1.18  fun metis_command type_sys i n (ls, ss) =
    1.19    using_labels ls ^ apply_on_subgoal "" i n ^ metis_call type_sys ss