# HG changeset patch
# User blanchet
# Date 1406280371 -7200
# Node ID cf20bdc83854da1a067beec1c3d1c873371b084e
# Parent  09d2b853b20c3b86de6b1fad3a3d025d5ef70bd4
more robustness in Isar proof construction

diff -r 09d2b853b20c -r cf20bdc83854 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jul 25 11:26:10 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jul 25 11:26:11 2014 +0200
@@ -218,8 +218,6 @@
       |> Config.put show_sorts false
       |> Config.put show_consts false
 
-    val register_fixes = map Free #> fold Variable.auto_fixes
-
     fun add_str s' = apfst (suffix s')
 
     fun of_indent ind = replicate_string (ind * indent_size) " "
@@ -246,7 +244,7 @@
             |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
             |> simplify_spaces
             |> maybe_quote),
-       ctxt |> Variable.auto_fixes term)
+       ctxt |> perhaps (try (Variable.auto_fixes term)))
 
     fun using_facts [] [] = ""
       | using_facts ls ss = enclose "using " " " (space_implode " " (map string_of_label ls @ ss))
@@ -266,7 +264,7 @@
       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)
+      (s ^ space_implode " and " (map of_free xs), ctxt |> fold Variable.auto_fixes (map Free xs))
 
     fun add_fix _ [] = I
       | add_fix ind xs = add_str (of_indent ind ^ "fix ") #> add_frees xs #> add_str "\n"