# HG changeset patch
# User smolkas
# Date 1370995089 14400
# Node ID 0b395800fdf0d0dfeda1b738c9c3a4b538a8e3ba
# Parent  13ca6876f74870abf11c17fb2290512dec19eedf
uncheck terms before annotation to avoid awkward syntax

diff -r 13ca6876f748 -r 0b395800fdf0 src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Tue Jun 11 19:11:31 2013 -0400
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Tue Jun 11 19:58:09 2013 -0400
@@ -2,8 +2,16 @@
     Author:     Jasmin Blanchette, TU Muenchen
     Author:     Steffen Juilf Smolka, TU Muenchen
 
-Supplement term with explicit type constraints that show up as
-type annotations when printing the term.
+Supplements term with a locally minmal, complete set of type constraints.
+Complete: The constraints suffice to infer the term's types.
+Minimal: Reducing the set of constraints further will make it incomplete.
+
+When configuring the pretty printer appropriately, the constraints will show up
+as type annotations when printing the term. This allows the term to be reparsed
+without a change of types.
+
+NOTE: Terms should be unchecked before calling annotate_types to avoid awkward
+syntax.
 *)
 
 signature SLEDGEHAMMER_ANNOTATE =
@@ -42,9 +50,14 @@
 
 (* (1) Generalize types *)
 fun generalize_types ctxt t =
-  t |> map_types (fn _ => dummyT)
-    |> Syntax.check_term
-         (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
+  let
+    val erase_types = map_types (fn _ => dummyT)
+    (* use schematic type variables *)
+    val ctxt = ctxt |> Proof_Context.set_mode Proof_Context.mode_pattern
+    val infer_types = singleton (Type_Infer_Context.infer_types ctxt)
+  in
+     t |> erase_types |> infer_types
+  end
 
 (* (2) Typing-spot table *)
 local
diff -r 13ca6876f748 -r 0b395800fdf0 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Jun 11 19:11:31 2013 -0400
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Jun 11 19:58:09 2013 -0400
@@ -463,8 +463,10 @@
       else
         of_show_have qs
     fun add_term term (s, ctxt) =
-      (s ^ (annotate_types ctxt term
-            |> with_vanilla_print_mode (Syntax.string_of_term ctxt)
+      (s ^ (term
+            |> singleton (Syntax.uncheck_terms ctxt)
+            |> annotate_types ctxt
+            |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
             |> simplify_spaces
             |> maybe_quote),
        ctxt |> Variable.auto_fixes term)