| changeset 19046 | bc5c6c9b114e |
| parent 18977 | f24c416a4814 |
| child 19473 | d87a8838afa4 |
--- a/src/Pure/Isar/context_rules.ML Wed Feb 15 19:11:10 2006 +0100 +++ b/src/Pure/Isar/context_rules.ML Wed Feb 15 21:34:55 2006 +0100 @@ -59,7 +59,7 @@ (elim_queryK, "extra elimination rules (elim?)")]; val rule_kinds = map #1 kind_names; -val rule_indexes = gen_distinct (op =) (map #1 rule_kinds); +val rule_indexes = distinct (op =) (map #1 rule_kinds); (* context data *)