# HG changeset patch
# User blanchet
# Date 1304291124 -7200
# Node ID 13c7194a896a48369b9e85a7903a0f86b5350599
# Parent  62398fdbb5287f2cc4525ea4dca43404f5655ea2
tuning

diff -r 62398fdbb528 -r 13c7194a896a src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Mon May 02 01:05:14 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Mon May 02 01:05:24 2011 +0200
@@ -196,7 +196,7 @@
   | using_labels ls =
     "using " ^ space_implode " " (map string_for_label ls) ^ " "
 fun metis_name full_types = if full_types then "metisFT" else "metis"
-fun metis_call full_types ss = command_call "metis" ss
+fun metis_call full_types ss = command_call (metis_name full_types) ss
 fun metis_command full_types i n (ls, ss) =
   using_labels ls ^ apply_on_subgoal "" i n ^ metis_call full_types ss
 fun minimize_line _ [] = ""
@@ -972,7 +972,7 @@
            |> then_chain_proof
            |> kill_useless_labels_in_proof
            |> relabel_proof
-           |> string_for_proof ctxt type_sys i n of
+           |> string_for_proof ctxt (is_type_sys_fairly_sound type_sys) i n of
         "" => "\nNo structured proof available (proof too short)."
       | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
     val isar_proof =