freeze types in Sledgehammer goal, not just terms

--- a/src/HOL/Tools/ATP/atp_problem.ML	Mon May 20 11:49:56 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon May 20 12:35:29 2013 +0200
@@ -851,7 +851,7 @@
      s
    else
      s |> no_qualifiers
-       |> perhaps (try (unprefix "'"))
+       |> unquote_tvar
        |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
        |> (fn s =>
               if size s > max_readable_name_size then

--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon May 20 11:49:56 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon May 20 12:35:29 2013 +0200
@@ -216,6 +216,7 @@
 (* Freshness almost guaranteed! *)
 val atp_prefix = "ATP" ^ Long_Name.separator
 val atp_weak_prefix = "ATP:"
+val atp_weak_suffix = ":ATP"
 
 val lam_lifted_prefix = atp_weak_prefix ^ "Lam"
 val lam_lifted_mono_prefix = lam_lifted_prefix ^ "m"
@@ -376,8 +377,8 @@
 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
 
-fun make_tvar (s, i) = tvar_prefix ^ ascii_of_indexname (unprefix "'" s, i)
-fun make_tfree s = tfree_prefix ^ ascii_of (unprefix "'" s)
+fun make_tvar (s, i) = tvar_prefix ^ ascii_of_indexname (unquote_tvar s, i)
+fun make_tfree s = tfree_prefix ^ ascii_of (unquote_tvar s)
 fun tvar_name ((x as (s, _)), _) = (make_tvar x, s)
 
 (* "HOL.eq" and choice are mapped to the ATP's equivalents *)
@@ -1260,12 +1261,18 @@
    same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
 fun freeze_term t =
   let
+    (* Freshness is desirable for completeness, but not for soundness. *)
+    fun indexed_name (s, i) = s ^ "_" ^ string_of_int i ^ atp_weak_suffix
     fun freeze (t $ u) = freeze t $ freeze u
       | freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
-      | freeze (Var ((s, i), T)) =
-        Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
+      | freeze (Var (x, T)) = Free (indexed_name x, T)
       | freeze t = t
-  in t |> exists_subterm is_Var t ? freeze end
+    fun freeze_tvar (x, S) = TFree (indexed_name x, S)
+  in
+    t |> exists_subterm is_Var t ? freeze
+      |> exists_type (exists_subtype is_TVar) t
+         ? map_types (map_type_tvar freeze_tvar)
+  end
 
 fun presimp_prop ctxt type_enc t =
   let

--- a/src/HOL/Tools/ATP/atp_util.ML	Mon May 20 11:49:56 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Mon May 20 12:35:29 2013 +0200
@@ -15,6 +15,7 @@
   val strip_spaces_except_between_idents : string -> string
   val elide_string : int -> string -> string
   val nat_subscript : int -> string
+  val unquote_tvar : string -> string
   val unyxml : string -> string
   val maybe_quote : string -> string
   val string_of_ext_time : bool * Time.time -> string
@@ -124,13 +125,16 @@
 fun nat_subscript n =
   n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
 
+val unquote_tvar = perhaps (try (unprefix "'"))
+val unquery_var = perhaps (try (unprefix "?"))
+
 val unyxml = XML.content_of o YXML.parse_body
 
 val is_long_identifier = forall Symbol_Pos.is_identifier o Long_Name.explode
 fun maybe_quote y =
   let val s = unyxml y in
-    y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
-           not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
+    y |> ((not (is_long_identifier (unquote_tvar s)) andalso
+           not (is_long_identifier (unquery_var s))) orelse
            Keyword.is_keyword s) ? quote
   end