src/Pure/Isar/specification.ML
changeset 27858 d385b67f8439
parent 26595 855893d4d75f
child 28080 4723eb2456ce
     1.1 --- a/src/Pure/Isar/specification.ML	Wed Aug 13 20:57:31 2008 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Wed Aug 13 20:57:33 2008 +0200
     1.3 @@ -224,7 +224,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.present_results lthy' ((kind, ""), res);
     1.8 +    val _ = ProofDisplay.theory_results lthy' ((kind, ""), res);
     1.9    in (res, lthy') end;
    1.10  
    1.11  val theorems = gen_theorems (K I) (K I);
    1.12 @@ -323,7 +323,7 @@
    1.13          lthy
    1.14          |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
    1.15          |> (fn (res, lthy') =>
    1.16 -          (ProofDisplay.present_results lthy' ((kind, name), res);
    1.17 +          (ProofDisplay.theory_results lthy' ((kind, name), res);
    1.18              if name = "" andalso null atts then lthy'
    1.19              else #2 (LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])] lthy')))
    1.20          |> after_qed results'