author | haftmann |
Tue, 05 Jun 2007 19:22:01 +0200 | |
changeset 23262 | 0fafccb015e6 |
parent 23261 | 85f27f79232f |
child 23263 | 0c227412b285 |
--- a/src/HOL/Tools/meson.ML Tue Jun 05 19:19:30 2007 +0200 +++ b/src/HOL/Tools/meson.ML Tue Jun 05 19:22:01 2007 +0200 @@ -238,7 +238,7 @@ fun resop nf [prem] = resolve_tac (nf prem) 1; (*Any need to extend this list with - "HOL.type_class","Code_Generator.eq_class","ProtoPure.term"?*) + "HOL.type_class","HOL.eq_class","ProtoPure.term"?*) val has_meta_conn = exists_Const (member (op =) ["==", "==>", "all", "prop"] o #1);