diff -r 7d97f60293ae -r 04e21a27c0ad src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Thu Sep 08 16:08:50 2005 +0200 +++ b/src/Pure/Isar/context_rules.ML Thu Sep 08 16:09:23 2005 +0200 @@ -111,7 +111,7 @@ fun print_rules prt x (Rules {rules, ...}) = let fun prt_kind (i, b) = - Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":") + Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":") (List.mapPartial (fn (_, (k, th)) => if k = (i, b) then SOME (prt x th) else NONE) (sort (int_ord o pairself fst) rules)); in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;