# HG changeset patch
# User smolkas
# Date 1370981599 14400
# Node ID ff89424b5094cacbd3bf30cd3dd8b3d78c58b8eb
# Parent  95186e6e4bf4bb502414246c16d3d3e83a14316b
make use of show_type_emphasis instead of using hack; make sure global configurations don't affect proof script creation

diff -r 95186e6e4bf4 -r ff89424b5094 src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Tue Jun 11 21:07:53 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Tue Jun 11 16:13:19 2013 -0400
@@ -34,19 +34,6 @@
 fun post_fold_term_type f s t =
   post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd
 
-local
-fun natify_numeral' (t as Const (s, T)) =
-    (case s of
-      "Groups.zero_class.zero" => Const (s, @{typ "nat"})
-    | "Groups.one_class.one" => Const (s, @{typ "nat"})
-    | "Num.numeral_class.numeral" => Const(s, @{typ "num"} --> @{typ "nat"})
-    | "Num.numeral_class.neg_numeral" => Const(s, @{typ "num"} --> @{typ "nat"})
-    | _ => t)
-  | natify_numeral' t = t
-in
-val natify_numerals = Term.map_aterms natify_numeral'
-end
-
 (* Data structures, orders *)
 val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
 structure Var_Set_Tab = Table(
@@ -157,9 +144,7 @@
         else (Type.constraint T t, (cp + 1, annots'))
       | post2 t _ x = (t, x)
   in
-    t |> natify_numerals (* typing all numerals as "nat"s prevents the pretty
-         printer from inserting additional, unwanted type annotations *)
-      |> post_traverse_term_type post2 (0, rev annots)
+    t |> post_traverse_term_type post2 (0, rev annots)
       |> fst
   end
 
diff -r 95186e6e4bf4 -r ff89424b5094 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jun 11 21:07:53 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jun 11 16:13:19 2013 -0400
@@ -369,8 +369,6 @@
 
 fun hammer_away override_params subcommand opt_i fact_override state =
   let
-    (* necessary to avoid problems in jedit *)
-    val state = state |> Proof.map_context (Config.put show_markup false)
     val ctxt = Proof.context_of state
     val override_params = override_params |> map (normalize_raw_param ctxt)
     val _ = Isabelle_System.mkdir (Path.explode (getenv "ISABELLE_TMP"))
diff -r 95186e6e4bf4 -r ff89424b5094 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Jun 11 21:07:53 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Jun 11 16:13:19 2013 -0400
@@ -433,6 +433,14 @@
 
 fun string_of_proof ctxt type_enc lam_trans i n proof =
   let
+    val ctxt =
+      (* make sure type constraint are actually printed *)
+      ctxt |> Config.put show_markup false
+      (* make sure only type constraints inserted by sh_annotate are printed *)
+           |> Config.put Printer.show_type_emphasis false
+           |> Config.put show_types false
+           |> Config.put show_sorts false
+           |> Config.put show_consts false
     val register_fixes = map Free #> fold Variable.auto_fixes
     fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
     fun of_indent ind = replicate_string (ind * indent_size) " "