src/Pure/Isar/isar_cmd.ML
changeset 64986 b81a048960a3
parent 63624 994d1a1105ef
child 67147 dea94b1aabc3
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Feb 04 20:12:27 2017 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Feb 04 21:15:11 2017 +0100
     1.3 @@ -260,21 +260,7 @@
     1.4      | SOME srcs =>
     1.5          let
     1.6            val ctxt = Toplevel.context_of state;
     1.7 -          val thy = Proof_Context.theory_of ctxt;
     1.8 -          fun pretty_proof thm =
     1.9 -            let
    1.10 -              val (_, prop) =
    1.11 -                Logic.unconstrainT (Thm.shyps_of thm)
    1.12 -                  (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
    1.13 -            in
    1.14 -              Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm))
    1.15 -              |> Reconstruct.reconstruct_proof ctxt prop
    1.16 -              |> Reconstruct.expand_proof ctxt [("", NONE)]
    1.17 -              |> Proofterm.rew_proof thy
    1.18 -              |> Proofterm.no_thm_proofs
    1.19 -              |> not full ? Proofterm.shrink_proof
    1.20 -              |> Proof_Syntax.pretty_proof ctxt
    1.21 -            end;
    1.22 +          val pretty_proof = Proof_Syntax.pretty_clean_proof_of ctxt full;
    1.23          in Pretty.chunks (map pretty_proof (Attrib.eval_thms ctxt srcs)) end);
    1.24  
    1.25  fun string_of_prop ctxt s =