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"