src/Pure/goal_display.ML
changeset 61268 abe08fb15a12
parent 61039 80f40d89dab6
child 64556 851ae0e7b09c
     1.1 --- a/src/Pure/goal_display.ML	Fri Sep 25 20:04:25 2015 +0200
     1.2 +++ b/src/Pure/goal_display.ML	Fri Sep 25 20:37:59 2015 +0200
     1.3 @@ -11,9 +11,6 @@
     1.4    val goals_limit: int Config.T
     1.5    val show_main_goal_raw: Config.raw
     1.6    val show_main_goal: bool Config.T
     1.7 -  val show_consts_raw: Config.raw
     1.8 -  val show_consts: bool Config.T
     1.9 -  val pretty_flexpair: Proof.context -> term * term -> Pretty.T
    1.10    val pretty_goals: Proof.context -> thm -> Pretty.T list
    1.11    val pretty_goal: Proof.context -> thm -> Pretty.T
    1.12    val string_of_goal: Proof.context -> thm -> string
    1.13 @@ -28,12 +25,6 @@
    1.14  val show_main_goal_raw = Config.declare_option ("show_main_goal", @{here});
    1.15  val show_main_goal = Config.bool show_main_goal_raw;
    1.16  
    1.17 -val show_consts_raw = Config.declare_option ("show_consts", @{here});
    1.18 -val show_consts = Config.bool show_consts_raw;
    1.19 -
    1.20 -fun pretty_flexpair ctxt (t, u) = Pretty.block
    1.21 -  [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
    1.22 -
    1.23  
    1.24  (*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
    1.25  
    1.26 @@ -107,7 +98,7 @@
    1.27        Pretty.markup (Markup.subgoal s) [Pretty.str (" " ^ s ^ ". "), prt_term A];
    1.28      val pretty_subgoals = map_index (fn (i, A) => pretty_subgoal (string_of_int (i + 1)) A);
    1.29  
    1.30 -    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
    1.31 +    val pretty_ffpairs = pretty_list "flex-flex pairs:" (Thm.pretty_flexpair ctxt);
    1.32  
    1.33      val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
    1.34      val pretty_vars = pretty_list "variables:" prt_vars o vars_of;