--- 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)
--- 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)
--- 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)
--- 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