src/Pure/display.ML
changeset 22846 fb79144af9a3
parent 21721 908a93216f00
child 22878 ca2eb5eb615b
     1.1 --- a/src/Pure/display.ML	Sun May 06 21:50:17 2007 +0200
     1.2 +++ b/src/Pure/display.ML	Mon May 07 00:49:59 2007 +0200
     1.3 @@ -234,9 +234,6 @@
     1.4      val rests = restricts |> map (apfst (apfst extern_const)) |> sort_wrt (#1 o #1);
     1.5    in
     1.6      [Pretty.strs ("names:" :: Context.names_of thy)] @
     1.7 -    (if verbose then
     1.8 -      [Pretty.strs ("theory data:" :: Context.theory_data_of thy),
     1.9 -       Pretty.strs ("proof data:" :: Context.proof_data_of thy)] else []) @
    1.10      [Pretty.strs ["name prefix:", NameSpace.path_of naming],
    1.11        Pretty.big_list "classes:" (map pretty_classrel clsses),
    1.12        pretty_default default,