src/Pure/Isar/proof_context.ML
changeset 6721 dcee829f8e21
parent 6560 1436349f8b28
child 6762 a9a515a43ae0
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon May 24 21:54:34 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon May 24 21:55:34 1999 +0200
     1.3 @@ -113,7 +113,10 @@
     1.4    let
     1.5      fun pretty_itms (name, [x]) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt x]
     1.6        | pretty_itms (name, xs) = Pretty.big_list (name ^ ":") (map prt xs);
     1.7 -  in Pretty.writeln (Pretty.big_list name (map pretty_itms items)) end;
     1.8 +  in
     1.9 +    if null items andalso not (! verbose) then ()
    1.10 +    else Pretty.writeln (Pretty.big_list name (map pretty_itms items))
    1.11 +  end;
    1.12  
    1.13  
    1.14  (* term bindings *)
    1.15 @@ -128,7 +131,10 @@
    1.16        | Some x' => if i = 0 then "??" ^ x' else Syntax.string_of_vname (x, i));
    1.17      fun pretty_bind (xi, (t, T)) = Pretty.block
    1.18        [Pretty.str (fix_var xi), Pretty.str " ==", Pretty.brk 1, prt_term t];
    1.19 -  in Pretty.writeln (Pretty.big_list "Term bindings:" (map pretty_bind (Vartab.dest binds))) end;
    1.20 +  in
    1.21 +    if Vartab.is_empty binds andalso not (! verbose) then ()
    1.22 +    else Pretty.writeln (Pretty.big_list "Term bindings:" (map pretty_bind (Vartab.dest binds)))
    1.23 +  end;
    1.24  
    1.25  
    1.26  (* local theorems *)
    1.27 @@ -169,7 +175,8 @@
    1.28      val prt_defS = prt_atom prt_varT prt_sort;
    1.29    in
    1.30      verb Pretty.writeln pretty_thy;
    1.31 -    Pretty.writeln (Pretty.big_list "Fixed variables:" (map prt_fix (rev fixes)));
    1.32 +    if null fixes andalso not (! verbose) then ()
    1.33 +    else Pretty.writeln (Pretty.big_list "Fixed variables:" (map prt_fix (rev fixes)));
    1.34      print_items (prt_term o #prop o Thm.rep_thm) "Assumptions:" assumes;
    1.35      verb print_binds ctxt;
    1.36      verb print_thms ctxt;