src/Pure/Isar/find_theorems.ML
changeset 29858 c8cee17d7e50
parent 29857 2cc976ed8a3c
child 29882 29154e67731d
     1.1 --- a/src/Pure/Isar/find_theorems.ML	Wed Feb 11 14:48:14 2009 +1100
     1.2 +++ b/src/Pure/Isar/find_theorems.ML	Wed Feb 11 16:03:10 2009 +1100
     1.3 @@ -370,10 +370,6 @@
     1.4      val lim = the_default (! limit) opt_limit;
     1.5      val thms = Library.drop (len - lim, matches);
     1.6  
     1.7 -    fun prt_fact (thmref, thm) = Pretty.block
     1.8 -      [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
     1.9 -        ProofContext.pretty_thm ctxt thm];
    1.10 -
    1.11      val end_msg = " in " ^
    1.12                    (List.nth (String.tokens Char.isSpace (end_timing start), 3))
    1.13                    ^ " secs"
    1.14 @@ -386,7 +382,7 @@
    1.15            (if len <= lim then ""
    1.16             else " (" ^ string_of_int lim ^ " displayed)")
    1.17             ^ end_msg ^ ":"), Pretty.str ""] @
    1.18 -        map prt_fact thms)
    1.19 +        map Display.pretty_fact thms)
    1.20      |> Pretty.chunks |> Pretty.writeln
    1.21    end
    1.22