src/Pure/Isar/context_rules.ML
changeset 32091 30e2ffbba718
parent 30529 23d1892f8015
child 32784 1a5dde5079ac
     1.1 --- a/src/Pure/Isar/context_rules.ML	Tue Jul 21 00:56:19 2009 +0200
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Tue Jul 21 01:03:18 2009 +0200
     1.3 @@ -116,7 +116,7 @@
     1.4      fun prt_kind (i, b) =
     1.5        Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
     1.6          (map_filter (fn (_, (k, th)) =>
     1.7 -            if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE)
     1.8 +            if k = (i, b) then SOME (Display.pretty_thm ctxt th) else NONE)
     1.9            (sort (int_ord o pairself fst) rules));
    1.10    in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
    1.11