1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Feb 02 20:53:51 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Feb 02 20:53:51 2014 +0100
     1.3 @@ -270,7 +270,7 @@
     1.4  
     1.5          val trace = Config.get ctxt trace
     1.6  
     1.7 -        val isar_proof =
     1.8 +        val canonical_isar_proof =
     1.9            refute_graph
    1.10            |> trace ? tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
    1.11            |> redirect_graph axioms tainted bot
    1.12 @@ -279,9 +279,13 @@
    1.13            |> postprocess_isar_proof_remove_unreferenced_steps I
    1.14            |> relabel_isar_proof_canonically
    1.15  
    1.16 +        val preplay_ctxt = ctxt
    1.17 +          |> enrich_context_with_local_facts canonical_isar_proof
    1.18 +          |> silence_reconstructors debug
    1.19 +
    1.20          val preplay_data as {preplay_outcome, overall_preplay_outcome, ...} =
    1.21 -          preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans preplay_timeout
    1.22 -            isar_proof
    1.23 +          preplay_data_of_isar_proof preplay_ctxt metis_type_enc metis_lam_trans preplay_timeout
    1.24 +            canonical_isar_proof
    1.25  
    1.26          fun str_of_preplay_outcome outcome =
    1.27            if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
    1.28 @@ -298,7 +302,7 @@
    1.29              ()
    1.30  
    1.31          val (play_outcome, isar_proof) =
    1.32 -          isar_proof
    1.33 +          canonical_isar_proof
    1.34            |> tap (trace_isar_proof "Original")
    1.35            |> compress_isar_proof compress_isar preplay_data
    1.36            |> tap (trace_isar_proof "Compressed")
    1.37 @@ -351,7 +355,7 @@
    1.38    | Not_Played => false)
    1.39  
    1.40  fun proof_text ctxt debug isar_proofs isar_params num_chained
    1.41 -               (one_line_params as (preplay, _, _, _, _, _)) =
    1.42 +    (one_line_params as (preplay, _, _, _, _, _)) =
    1.43    (if isar_proofs = SOME true orelse
    1.44        (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
    1.45       isar_proof_text ctxt debug isar_proofs isar_params