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

--- 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 ^ " :: " ^