# HG changeset patch
# User wenzelm
# Date 1220386820 -7200
# Node ID d81a4ed6b538d3b3e27c37329df8e5469dd4ae12
# Parent  5886e9359aa8f06c0528d5f651d12c51bb64563c
ProofDisplay.print_results;

diff -r 5886e9359aa8 -r d81a4ed6b538 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue Sep 02 22:20:16 2008 +0200
+++ b/src/Pure/Isar/specification.ML	Tue Sep 02 22:20:20 2008 +0200
@@ -235,7 +235,7 @@
       ((name, map attrib atts),
         bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
     val (res, lthy') = lthy |> LocalTheory.notes kind facts;
-    val _ = ProofDisplay.theory_results lthy' ((kind, ""), res);
+    val _ = ProofDisplay.print_results true lthy' ((kind, ""), res);
   in (res, lthy') end;
 
 val theorems = gen_theorems (K I) (K I);
@@ -337,12 +337,12 @@
         |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
         |> (fn (res, lthy') =>
           if Name.name_of name = "" andalso null atts then
-            (ProofDisplay.theory_results lthy' ((kind, ""), res); lthy')
+            (ProofDisplay.print_results true lthy' ((kind, ""), res); lthy')
           else
             let
               val ([(res_name, _)], lthy'') = lthy'
                 |> LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])];
-              val _ = ProofDisplay.theory_results lthy' ((kind, res_name), res);
+              val _ = ProofDisplay.print_results true lthy' ((kind, res_name), res);
             in lthy'' end)
         |> after_qed results'
       end;