# HG changeset patch
# User wenzelm
# Date 1235915123 -3600
# Node ID 1f836e949ac26284f768c9c2866b3d09a0a18686
# Parent  6889bfc0380471d1abfeb7c4af3f5a9796d02033
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;

diff -r 6889bfc03804 -r 1f836e949ac2 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Sun Mar 01 14:36:27 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Sun Mar 01 14:45:23 2009 +0100
@@ -6,16 +6,14 @@
 
 signature FIND_THEOREMS =
 sig
-  val limit: int ref
-  val tac_limit: int ref
-
   datatype 'term criterion =
     Name of string | Intro | Elim | Dest | Solves | Simp of 'term |
     Pattern of 'term
-
+  val tac_limit: int ref
+  val limit: int ref
   val find_theorems: Proof.context -> thm option -> bool ->
     (bool * string criterion) list -> (Facts.ref * thm) list
-
+  val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
   val print_theorems: Proof.context -> thm option -> int option -> bool ->
     (bool * string criterion) list -> unit
 end;
@@ -344,8 +342,7 @@
 
 fun find_theorems ctxt opt_goal rem_dups raw_criteria =
   let
-    val add_prems = Seq.hd o (TRY (Method.insert_tac
-                                     (Assumption.prems_of ctxt) 1));
+    val add_prems = Seq.hd o (TRY (Method.insert_tac (Assumption.prems_of ctxt) 1));
     val opt_goal' = Option.map add_prems opt_goal;
 
     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
@@ -359,6 +356,11 @@
       else raw_matches;
   in matches end;
 
+
+fun pretty_thm ctxt (thmref, thm) = Pretty.block
+  [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
+    ProofContext.pretty_thm ctxt thm];
+
 fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
   let
     val start = start_timing ();
@@ -382,7 +384,7 @@
           (if len <= lim then ""
            else " (" ^ string_of_int lim ^ " displayed)")
            ^ end_msg ^ ":"), Pretty.str ""] @
-        map Display.pretty_fact thms)
+        map (pretty_thm ctxt) thms)
     |> Pretty.chunks |> Pretty.writeln
   end;
 
diff -r 6889bfc03804 -r 1f836e949ac2 src/Pure/display.ML
--- a/src/Pure/display.ML	Sun Mar 01 14:36:27 2009 +0100
+++ b/src/Pure/display.ML	Sun Mar 01 14:45:23 2009 +0100
@@ -20,7 +20,6 @@
   val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
   val pretty_thm: thm -> Pretty.T
   val string_of_thm: thm -> string
-  val pretty_fact: Facts.ref * thm -> Pretty.T
   val pretty_thms: thm list -> Pretty.T
   val pretty_thm_sg: theory -> thm -> Pretty.T
   val pretty_thms_sg: theory -> thm list -> Pretty.T
@@ -93,10 +92,6 @@
 
 val string_of_thm = Pretty.string_of o pretty_thm;
 
-fun pretty_fact (thmref, thm) = Pretty.block
-  [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
-   pretty_thm thm];
-
 fun pretty_thms [th] = pretty_thm th
   | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
 
diff -r 6889bfc03804 -r 1f836e949ac2 src/Tools/auto_solve.ML
--- a/src/Tools/auto_solve.ML	Sun Mar 01 14:36:27 2009 +0100
+++ b/src/Tools/auto_solve.ML	Sun Mar 01 14:45:23 2009 +0100
@@ -45,7 +45,7 @@
                   | SOME g => Syntax.string_of_term ctxt (term_of g);
       in
         Pretty.big_list (msg ^ " could be solved directly with:")
-                        (map Display.pretty_fact results)
+                        (map (FindTheorems.pretty_thm ctxt) results)
       end;
 
     fun seek_against_goal () =