src/Pure/Isar/proof_context.ML
changeset 21583 6fb553dc039b
parent 21569 a0d0ea84521d
child 21593 282c40fb001a
equal deleted inserted replaced
21582:ac6af184bfb0 21583:6fb553dc039b
   315 fun pretty_thm ctxt th =
   315 fun pretty_thm ctxt th =
   316   let
   316   let
   317     val thy = theory_of ctxt;
   317     val thy = theory_of ctxt;
   318     val (pp, asms) =
   318     val (pp, asms) =
   319       if Theory.eq_thy (thy, ProtoPure.thy) then (Sign.pp thy, [])
   319       if Theory.eq_thy (thy, ProtoPure.thy) then (Sign.pp thy, [])
   320       else (pp ctxt, Assumption.assms_of ctxt);
   320       else (pp ctxt, map Thm.term_of (Assumption.assms_of ctxt));
   321   in Display.pretty_thm_aux pp false true asms th end;
   321   in Display.pretty_thm_aux pp false true asms th end;
   322 
   322 
   323 fun pretty_thms ctxt [th] = pretty_thm ctxt th
   323 fun pretty_thms ctxt [th] = pretty_thm ctxt th
   324   | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
   324   | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
   325 
   325