src/Pure/Isar/isar_cmd.ML
changeset 57605 8e0a7eaffe47
parent 56868 b5fb264d53ba
child 57683 cc0aa6528890
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Jul 22 13:36:51 2014 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Jul 22 14:03:00 2014 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4    val ml_diag: bool -> Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
     1.5    val diag_state: Proof.context -> Toplevel.state
     1.6    val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
     1.7 -  val pretty_theorems: bool -> Toplevel.state -> Pretty.T
     1.8 +  val pretty_theorems: bool -> Toplevel.state -> Pretty.T list
     1.9    val thy_deps: Toplevel.transition -> Toplevel.transition
    1.10    val locale_deps: Toplevel.transition -> Toplevel.transition
    1.11    val class_deps: Toplevel.transition -> Toplevel.transition
    1.12 @@ -262,7 +262,7 @@
    1.13  
    1.14  fun pretty_theorems verbose st =
    1.15    if Toplevel.is_proof st then
    1.16 -    Pretty.chunks (Proof_Context.pretty_local_facts (Toplevel.context_of st) verbose)
    1.17 +    Proof_Context.pretty_local_facts (Toplevel.context_of st) verbose
    1.18    else
    1.19      let
    1.20        val thy = Toplevel.theory_of st;