# HG changeset patch
# User blanchet
# Date 1351679001 -3600
# Node ID 90e7be285b497a7e5eac616e0b26e1c5a809e9b7
# Parent  5b4b0e4e5205a382bb0ea2a63935d5cdfb673048
took out "using only ..." comments in Sledgehammer generated metis/smt calls, until these can be generated soundly

diff -r 5b4b0e4e5205 -r 90e7be285b49 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Oct 31 11:23:21 2012 +0100
@@ -205,11 +205,13 @@
 fun show_time NONE = ""
   | show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")"
 
+(* FIXME: Various bugs, esp. with "unfolding"
 fun unusing_chained_facts _ 0 = ""
   | unusing_chained_facts used_chaineds num_chained =
     if length used_chaineds = num_chained then ""
     else if null used_chaineds then "(* using no facts *) "
     else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
+*)
 
 fun apply_on_subgoal _ 1 = "by "
   | apply_on_subgoal 1 _ = "apply "
@@ -225,7 +227,7 @@
   | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
 
 fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
-  unusing_chained_facts used_chaineds num_chained ^
+  (* unusing_chained_facts used_chaineds num_chained ^ *)
   using_labels ls ^ apply_on_subgoal i n ^
   command_call (string_for_reconstructor reconstr) ss