src/Pure/display.ML
changeset 13658 c9ad3e64ddcf
parent 12831 a2a3896f9c48
child 14178 14a12da7288e
     1.1 --- a/src/Pure/display.ML	Mon Oct 21 17:00:45 2002 +0200
     1.2 +++ b/src/Pure/display.ML	Mon Oct 21 17:04:47 2002 +0200
     1.3 @@ -28,6 +28,7 @@
     1.4  signature DISPLAY =
     1.5  sig
     1.6    include BASIC_DISPLAY
     1.7 +  val pretty_flexpair: (term -> Pretty.T) -> term * term -> Pretty.T
     1.8    val pretty_thm_aux: (sort -> Pretty.T) * (term -> Pretty.T) -> bool -> thm -> Pretty.T
     1.9    val pretty_thm_no_quote: thm -> Pretty.T
    1.10    val pretty_thm: thm -> Pretty.T
    1.11 @@ -66,20 +67,25 @@
    1.12  fun pretty_tag (name, args) = Pretty.strs (name :: map quote args);
    1.13  val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    1.14  
    1.15 +fun pretty_flexpair pretty_term (t, u) = Pretty.block
    1.16 +  [pretty_term t, Pretty.str " =?=", Pretty.brk 1, pretty_term u];
    1.17 +
    1.18  fun pretty_thm_aux (pretty_sort, pretty_term) quote th =
    1.19    let
    1.20 -    val {hyps, prop, der = (ora, _), ...} = rep_thm th;
    1.21 +    val {hyps, tpairs, prop, der = (ora, _), ...} = rep_thm th;
    1.22      val xshyps = Thm.extra_shyps th;
    1.23      val (_, tags) = Thm.get_name_tags th;
    1.24  
    1.25 -    val prt_term = (if quote then Pretty.quote else I) o pretty_term;
    1.26 +    val q = if quote then Pretty.quote else I;
    1.27 +    val prt_term = q o pretty_term;
    1.28  
    1.29 -    val hlen = length xshyps + length hyps;
    1.30 +    val hlen = length xshyps + length hyps + length tpairs;
    1.31      val hsymbs =
    1.32        if hlen = 0 andalso not ora then []
    1.33        else if ! show_hyps then
    1.34          [Pretty.brk 2, Pretty.list "[" "]"
    1.35 -          (map prt_term hyps @ map pretty_sort xshyps @
    1.36 +          (map (q o pretty_flexpair pretty_term) tpairs @ map prt_term hyps @
    1.37 +           map pretty_sort xshyps @
    1.38              (if ora then [Pretty.str "!"] else []))]
    1.39        else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^
    1.40          (if ora then "!" else "") ^ "]")];
    1.41 @@ -307,15 +313,15 @@
    1.42        Pretty.blk (0, [Pretty.str (begin_goal ^ " " ^ string_of_int n ^ ". "), prt_term A]);
    1.43      fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
    1.44  
    1.45 -    val pretty_ffpairs = pretty_list "flex-flex pairs:" (prt_term o Logic.mk_flexpair);
    1.46 +    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair prt_term);
    1.47  
    1.48      val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
    1.49      val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
    1.50      val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
    1.51  
    1.52  
    1.53 -    val {prop, ...} = rep_thm state;
    1.54 -    val (tpairs, As, B) = Logic.strip_horn prop;
    1.55 +    val {prop, tpairs, ...} = rep_thm state;
    1.56 +    val (As, B) = Logic.strip_horn prop;
    1.57      val ngoals = length As;
    1.58  
    1.59      fun pretty_gs (types, sorts) =