# HG changeset patch
# User blanchet
# Date 1387465880 -3600
# Node ID a127968726035656f68c8861bd2d9048603ba9af
# Parent  d9ab86c044fdc3925abfbada8a51fa87a0ed71c5
tuning

diff -r d9ab86c044fd -r a12796872603 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Dec 19 15:47:17 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Dec 19 16:11:20 2013 +0100
@@ -87,8 +87,7 @@
 fun metis_call type_enc lam_trans =
   let
     val type_enc =
-      (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases
-                      type_enc of
+      (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of
         [alias] => alias
       | _ => type_enc)
     val opts = [] |> type_enc <> partial_typesN ? cons type_enc
@@ -136,9 +135,8 @@
           (* The term could be an Isabelle variable or a variable from the ATP, say "X1" or "_5018".
              Sometimes variables from the ATP are indistinguishable from Isabelle variables, which
              forces us to use a type parameter in all cases. *)
-          Type_Infer.param 0 (a |> perhaps (unprefix_and_unascii tvar_prefix),
-            (if null clss then HOLogic.typeS
-             else map class_of_atp_class clss))))
+          Type_Infer.param 0 ("'" ^ perhaps (unprefix_and_unascii tvar_prefix) a,
+            (if null clss then HOLogic.typeS else map class_of_atp_class clss))))
   end
 
 fun atp_type_of_atp_term (ATerm ((s, _), us)) = AType ((s, []), map atp_type_of_atp_term us)
diff -r d9ab86c044fd -r a12796872603 src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Thu Dec 19 15:47:17 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Thu Dec 19 16:11:20 2013 +0100
@@ -94,7 +94,6 @@
 (* (3) handle trivial tfrees  *)
 fun handle_trivial_tfrees ctxt (t', subst) =
   let
-
     val add_tfree_names =
       snd #> snd #> fold_atyps (fn TFree (x, _) => cons x | _ => I)
 
@@ -134,8 +133,7 @@
 
 (* (4) Typing-spot table *)
 local
-fun key_of_atype (TVar (z, _)) =
-    Ord_List.insert indexname_ord z
+fun key_of_atype (TVar (z, _)) = Ord_List.insert indexname_ord z
   | key_of_atype _ = I
 fun key_of_type T = fold_atyps key_of_atype T []
 fun update_tab t T (tab, pos) =
@@ -180,8 +178,7 @@
 fun introduce_annotations subst spots t t' =
   let
     fun subst_atype (T as TVar (idxn, S)) subst =
-        (Envir.subst_type subst T,
-         Vartab.update (idxn, (S, dummyT)) subst)
+        (Envir.subst_type subst T, Vartab.update (idxn, (S, dummyT)) subst)
       | subst_atype T subst = (T, subst)
     val subst_type = fold_map_atypes subst_atype
     fun collect_annot _ T (subst, cp, ps as p :: ps', annots) =
@@ -195,8 +192,7 @@
     val (_, _, _, annots) =
       post_fold_term_type collect_annot (subst, 0, spots, []) t'
     fun insert_annot t _ (cp, annots as (p, T) :: annots') =
-        if p <> cp then (t, (cp + 1, annots))
-        else (Type.constraint T t, (cp + 1, annots'))
+        if p <> cp then (t, (cp + 1, annots)) else (Type.constraint T t, (cp + 1, annots'))
       | insert_annot t _ x = (t, x)
   in
     t |> post_traverse_term_type insert_annot (0, rev annots)
diff -r d9ab86c044fd -r a12796872603 src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Dec 19 15:47:17 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Dec 19 16:11:20 2013 +0100
@@ -145,7 +145,7 @@
     fun of_have qs nr =
       if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
         "ultimately " ^ of_show_have qs
-      else if nr=1 orelse member (op =) qs Then then
+      else if nr = 1 orelse member (op =) qs Then then
         of_thus_hence qs
       else
         of_show_have qs
@@ -189,8 +189,7 @@
 
     fun of_free (s, T) =
       maybe_quote s ^ " :: " ^
-      maybe_quote (simplify_spaces (with_vanilla_print_mode
-        (Syntax.string_of_typ ctxt) T))
+      maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T))
 
     fun add_frees xs (s, ctxt) =
       (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)
diff -r d9ab86c044fd -r a12796872603 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Dec 19 15:47:17 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Dec 19 16:11:20 2013 +0100
@@ -142,8 +142,7 @@
 val one_year = seconds (365.0 * 24.0 * 60.0 * 60.0)
 
 fun with_vanilla_print_mode f x =
-  Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
-                           (print_mode_value ())) f x
+  Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) f x
 
 fun hackish_string_of_term ctxt =
   with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces