# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID fdd15e889ad7717c0fe2d11a367a502efd244e72
# Parent  865ce93ce0257d4d1a58413b5af57b7416aa0b9b
no need to use metisFT for Isar proofs -- metis falls back on it anyway

diff -r 865ce93ce025 -r fdd15e889ad7 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu May 12 15:29:19 2011 +0200
@@ -908,7 +908,7 @@
         step :: aux subst depth nextp proof
   in aux [] 0 (1, 1) end
 
-fun string_for_proof ctxt0 type_sys i n =
+fun string_for_proof ctxt0 i n =
   let
     val ctxt = ctxt0
       |> Config.put show_free_types false
@@ -931,7 +931,7 @@
          if member (op =) qs Show then "show" else "have")
     val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
     fun do_facts (ls, ss) =
-      metis_command type_sys 1 1
+      metis_command false 1 1
                     (ls |> sort_distinct (prod_ord string_ord int_ord),
                      ss |> sort_distinct string_ord)
     and do_step ind (Fix xs) =
@@ -984,7 +984,7 @@
            |> then_chain_proof
            |> kill_useless_labels_in_proof
            |> relabel_proof
-           |> string_for_proof ctxt (is_type_sys_fairly_sound type_sys) i n of
+           |> string_for_proof ctxt i n of
         "" => "\nNo structured proof available (proof too short)."
       | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
     val isar_proof =