1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Jul 25 11:26:10 2014 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Jul 25 11:26:11 2014 +0200
1.3 @@ -218,8 +218,6 @@
1.4 |> Config.put show_sorts false
1.5 |> Config.put show_consts false
1.6
1.7 - val register_fixes = map Free #> fold Variable.auto_fixes
1.8 -
1.9 fun add_str s' = apfst (suffix s')
1.10
1.11 fun of_indent ind = replicate_string (ind * indent_size) " "
1.12 @@ -246,7 +244,7 @@
1.13 |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
1.14 |> simplify_spaces
1.15 |> maybe_quote),
1.16 - ctxt |> Variable.auto_fixes term)
1.17 + ctxt |> perhaps (try (Variable.auto_fixes term)))
1.18
1.19 fun using_facts [] [] = ""
1.20 | using_facts ls ss = enclose "using " " " (space_implode " " (map string_of_label ls @ ss))
1.21 @@ -266,7 +264,7 @@
1.22 maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T))
1.23
1.24 fun add_frees xs (s, ctxt) =
1.25 - (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)
1.26 + (s ^ space_implode " and " (map of_free xs), ctxt |> fold Variable.auto_fixes (map Free xs))
1.27
1.28 fun add_fix _ [] = I
1.29 | add_fix ind xs = add_str (of_indent ind ^ "fix ") #> add_frees xs #> add_str "\n"