merged

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Wed May 22 18:10:54 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Wed May 22 19:44:51 2013 +0200
@@ -34,6 +34,19 @@
 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(
@@ -143,7 +156,12 @@
         if p <> cp then (t, (cp + 1, annots))
         else (Type.constraint T t, (cp + 1, annots'))
       | post2 t _ x = (t, x)
-  in post_traverse_term_type post2 (0, rev annots) t |> fst end
+  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)
+      |> fst
+  end
 
 (* (5) Annotate *)
 fun annotate_types ctxt t =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Wed May 22 18:10:54 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Wed May 22 19:44:51 2013 +0200
@@ -9,7 +9,7 @@
 signature SLEDGEHAMMER_PROOF =
 sig
   type label = string * int
-  type facts = label list * string list
+  type facts = label list * string list (* local & global *)
 
   datatype isar_qualifier = Show | Then
 
@@ -68,8 +68,6 @@
 fun fix_of_proof (Proof (fix, _, _)) = fix
 fun assms_of_proof (Proof (_, assms, _)) = assms
 fun steps_of_proof (Proof (_, _, steps)) = steps
-(*fun map_steps_of_proof f (Proof (fix, assms, steps)) =
-  Proof(fix, assms, f steps)*)
 
 fun label_of_step (Obtain (_, _, l, _, _)) = SOME l
   | label_of_step (Prove (_, l, _, _)) = SOME l