# HG changeset patch
# User krauss
# Date 1298649464 -3600
# Node ID 6611b9cef38b7de1c3fe5c3b2092a57f4664ae1a
# Parent  b933142e02d0821d9ed19e6d50e6e857ca2d4ccb
reactivate time measurement (partly reverting c27b0b37041a);
export pretty_theorem, to display both internal or external facts

diff -r b933142e02d0 -r 6611b9cef38b src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Fri Feb 25 16:57:43 2011 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Fri Feb 25 16:57:44 2011 +0100
@@ -11,8 +11,7 @@
     Pattern of 'term
 
   datatype theorem =
-    Internal of Facts.ref * thm |
-    External of Facts.ref * term
+    Internal of Facts.ref * thm | External of Facts.ref * term
 
   val tac_limit: int Unsynchronized.ref
   val limit: int Unsynchronized.ref
@@ -22,7 +21,9 @@
     int option -> bool -> (bool * string criterion) list ->
     int option * theorem list
 
+  val pretty_theorem: Proof.context -> theorem -> Pretty.T
   val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
+
 end;
 
 structure Find_Theorems: FIND_THEOREMS =
@@ -80,7 +81,7 @@
   end;
 
 
-(** theorems, either internal or external (without proof) *)
+(** theorems, either internal or external (without proof) **)
 
 datatype theorem =
   Internal of Facts.ref * thm |
@@ -452,16 +453,23 @@
      rem_dups raw_criteria
   |> apsnd (map (fn Internal f => f));
 
-fun pretty_thm ctxt (thmref, thm) = Pretty.block
-  [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
-    Display.pretty_thm ctxt thm];
+fun pretty_theorem ctxt (Internal (thmref, thm)) = Pretty.block
+      [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
+        Display.pretty_thm ctxt thm]
+  | pretty_theorem ctxt (External (thmref, prop)) = Pretty.block
+      [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
+        Syntax.unparse_term ctxt prop];
 
-fun print_theorems ctxt (foundo, thms) raw_criteria =
+fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
+
+fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
   let
     val start = start_timing ();
 
     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
-    val returned = length thms;
+    val (foundo, theorems) = filter_theorems ctxt (map Internal (all_facts_of ctxt))
+      opt_goal opt_limit rem_dups raw_criteria;
+    val returned = length theorems;
 
     val tally_msg =
       (case foundo of
@@ -476,10 +484,10 @@
   in
     Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
     Pretty.str "" ::
-    (if null thms then [Pretty.str ("nothing found" ^ end_msg)]
+    (if null theorems then [Pretty.str ("nothing found" ^ end_msg)]
      else
       [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
-        map (pretty_thm ctxt) thms)
+        map (pretty_theorem ctxt) theorems)
   end |> Pretty.chunks |> Pretty.writeln;
 
 
@@ -515,8 +523,7 @@
           let
             val ctxt = Toplevel.context_of state;
             val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
-            val found = find_theorems ctxt opt_goal opt_lim rem_dups spec;
-          in print_theorems ctxt found spec end)));
+          in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
 
 end;