src/Pure/Isar/context_rules.ML
changeset 19482 9f11af8f7ef9
parent 19473 d87a8838afa4
child 20289 ba7a7c56bed5
     1.1 --- a/src/Pure/Isar/context_rules.ML	Thu Apr 27 12:11:56 2006 +0200
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Thu Apr 27 15:06:35 2006 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4        val ctxt = Context.proof_of generic;
     1.5        fun prt_kind (i, b) =
     1.6          Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
     1.7 -          (List.mapPartial (fn (_, (k, th)) =>
     1.8 +          (map_filter (fn (_, (k, th)) =>
     1.9                if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE)
    1.10              (sort (int_ord o pairself fst) rules));
    1.11      in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;