replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
authorwenzelm
Sun Mar 01 14:45:23 2009 +0100 (2009-03-01)
changeset 301861f836e949ac2
parent 30185 6889bfc03804
child 30187 b92b3375e919
replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
minor tuning according to Isabelle coding conventions;
src/Pure/Tools/find_theorems.ML
src/Pure/display.ML
src/Tools/auto_solve.ML
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Sun Mar 01 14:36:27 2009 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Sun Mar 01 14:45:23 2009 +0100
     1.3 @@ -6,16 +6,14 @@
     1.4  
     1.5  signature FIND_THEOREMS =
     1.6  sig
     1.7 -  val limit: int ref
     1.8 -  val tac_limit: int ref
     1.9 -
    1.10    datatype 'term criterion =
    1.11      Name of string | Intro | Elim | Dest | Solves | Simp of 'term |
    1.12      Pattern of 'term
    1.13 -
    1.14 +  val tac_limit: int ref
    1.15 +  val limit: int ref
    1.16    val find_theorems: Proof.context -> thm option -> bool ->
    1.17      (bool * string criterion) list -> (Facts.ref * thm) list
    1.18 -
    1.19 +  val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
    1.20    val print_theorems: Proof.context -> thm option -> int option -> bool ->
    1.21      (bool * string criterion) list -> unit
    1.22  end;
    1.23 @@ -344,8 +342,7 @@
    1.24  
    1.25  fun find_theorems ctxt opt_goal rem_dups raw_criteria =
    1.26    let
    1.27 -    val add_prems = Seq.hd o (TRY (Method.insert_tac
    1.28 -                                     (Assumption.prems_of ctxt) 1));
    1.29 +    val add_prems = Seq.hd o (TRY (Method.insert_tac (Assumption.prems_of ctxt) 1));
    1.30      val opt_goal' = Option.map add_prems opt_goal;
    1.31  
    1.32      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
    1.33 @@ -359,6 +356,11 @@
    1.34        else raw_matches;
    1.35    in matches end;
    1.36  
    1.37 +
    1.38 +fun pretty_thm ctxt (thmref, thm) = Pretty.block
    1.39 +  [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
    1.40 +    ProofContext.pretty_thm ctxt thm];
    1.41 +
    1.42  fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
    1.43    let
    1.44      val start = start_timing ();
    1.45 @@ -382,7 +384,7 @@
    1.46            (if len <= lim then ""
    1.47             else " (" ^ string_of_int lim ^ " displayed)")
    1.48             ^ end_msg ^ ":"), Pretty.str ""] @
    1.49 -        map Display.pretty_fact thms)
    1.50 +        map (pretty_thm ctxt) thms)
    1.51      |> Pretty.chunks |> Pretty.writeln
    1.52    end;
    1.53  
     2.1 --- a/src/Pure/display.ML	Sun Mar 01 14:36:27 2009 +0100
     2.2 +++ b/src/Pure/display.ML	Sun Mar 01 14:45:23 2009 +0100
     2.3 @@ -20,7 +20,6 @@
     2.4    val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
     2.5    val pretty_thm: thm -> Pretty.T
     2.6    val string_of_thm: thm -> string
     2.7 -  val pretty_fact: Facts.ref * thm -> Pretty.T
     2.8    val pretty_thms: thm list -> Pretty.T
     2.9    val pretty_thm_sg: theory -> thm -> Pretty.T
    2.10    val pretty_thms_sg: theory -> thm list -> Pretty.T
    2.11 @@ -93,10 +92,6 @@
    2.12  
    2.13  val string_of_thm = Pretty.string_of o pretty_thm;
    2.14  
    2.15 -fun pretty_fact (thmref, thm) = Pretty.block
    2.16 -  [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
    2.17 -   pretty_thm thm];
    2.18 -
    2.19  fun pretty_thms [th] = pretty_thm th
    2.20    | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
    2.21  
     3.1 --- a/src/Tools/auto_solve.ML	Sun Mar 01 14:36:27 2009 +0100
     3.2 +++ b/src/Tools/auto_solve.ML	Sun Mar 01 14:45:23 2009 +0100
     3.3 @@ -45,7 +45,7 @@
     3.4                    | SOME g => Syntax.string_of_term ctxt (term_of g);
     3.5        in
     3.6          Pretty.big_list (msg ^ " could be solved directly with:")
     3.7 -                        (map Display.pretty_fact results)
     3.8 +                        (map (FindTheorems.pretty_thm ctxt) results)
     3.9        end;
    3.10  
    3.11      fun seek_against_goal () =