1.1 --- a/src/Pure/Isar/specification.ML	Tue Sep 02 22:20:16 2008 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Tue Sep 02 22:20:20 2008 +0200
     1.3 @@ -235,7 +235,7 @@
     1.4        ((name, map attrib atts),
     1.5          bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
     1.6      val (res, lthy') = lthy |> LocalTheory.notes kind facts;
     1.7 -    val _ = ProofDisplay.theory_results lthy' ((kind, ""), res);
     1.8 +    val _ = ProofDisplay.print_results true lthy' ((kind, ""), res);
     1.9    in (res, lthy') end;
    1.10  
    1.11  val theorems = gen_theorems (K I) (K I);
    1.12 @@ -337,12 +337,12 @@
    1.13          |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
    1.14          |> (fn (res, lthy') =>
    1.15            if Name.name_of name = "" andalso null atts then
    1.16 -            (ProofDisplay.theory_results lthy' ((kind, ""), res); lthy')
    1.17 +            (ProofDisplay.print_results true lthy' ((kind, ""), res); lthy')
    1.18            else
    1.19              let
    1.20                val ([(res_name, _)], lthy'') = lthy'
    1.21                  |> LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])];
    1.22 -              val _ = ProofDisplay.theory_results lthy' ((kind, res_name), res);
    1.23 +              val _ = ProofDisplay.print_results true lthy' ((kind, res_name), res);
    1.24              in lthy'' end)
    1.25          |> after_qed results'
    1.26        end;