# HG changeset patch
# User wenzelm
# Date 1218653853 -7200
# Node ID d385b67f84395dfb08f84617571e04c8c8be17ee
# Parent  fdf43ffceae0f4c1fa8237e156169df50ce5a58f
ProofDisplay.theory_results;

diff -r fdf43ffceae0 -r d385b67f8439 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Aug 13 20:57:31 2008 +0200
+++ b/src/Pure/Isar/specification.ML	Wed Aug 13 20:57:33 2008 +0200
@@ -224,7 +224,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.present_results lthy' ((kind, ""), res);
+    val _ = ProofDisplay.theory_results lthy' ((kind, ""), res);
   in (res, lthy') end;
 
 val theorems = gen_theorems (K I) (K I);
@@ -323,7 +323,7 @@
         lthy
         |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
         |> (fn (res, lthy') =>
-          (ProofDisplay.present_results lthy' ((kind, name), res);
+          (ProofDisplay.theory_results lthy' ((kind, name), res);
             if name = "" andalso null atts then lthy'
             else #2 (LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])] lthy')))
         |> after_qed results'