Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
changeset 57792 9cb24c835284
parent 57791 d80d3fb56270
child 58061 3d060f43accb 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 05 10:17:15 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 05 10:59:40 2014 +0200
@@ -361,7 +361,8 @@
           ||> (comment_isar_proof comment_of
                #> chain_isar_proof
                #> kill_useless_labels_in_isar_proof
-               #> relabel_isar_proof_nicely)
+               #> relabel_isar_proof_nicely
+               #> rationalize_obtains_in_isar_proofs ctxt)
       in
         (case add_isar_steps (steps_of_isar_proof isar_proof) 0 of
           1 =>
isabelle