# HG changeset patch
# User blanchet
# Date 1275482152 -7200
# Node ID 42268dc7d6c47f4dabbdb5fb438e92ef72ea7f05
# Parent  32b3d16b04f67a6fb8936e4a3a3f78b39f62ce65
show types in Isar proofs, but not for free variables;
this makes proofs more robust, without as much clutter as there used to be when types were enabled previously

diff -r 32b3d16b04f6 -r 42268dc7d6c4 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jun 02 12:28:42 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jun 02 14:35:52 2010 +0200
@@ -914,9 +914,11 @@
 
 fun string_for_proof ctxt i n =
   let
-    fun fix_print_mode f =
-      Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
-                      (print_mode_value ())) f
+    fun fix_print_mode f x =
+      setmp_CRITICAL show_no_free_types true
+          (setmp_CRITICAL show_types true
+               (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+                                         (print_mode_value ())) f)) x
     fun do_indent ind = replicate_string (ind * indent_size) " "
     fun do_free (s, T) =
       maybe_quote s ^ " :: " ^