author wenzelm Tue Sep 02 22:20:20 2008 +0200 (2008-09-02) changeset 28093 d81a4ed6b538 parent 28092 5886e9359aa8 child 28094 5f340fb49b90
ProofDisplay.print_results;
```     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;
```