eliminated Code_Generator.thy
authorhaftmann
Tue, 05 Jun 2007 19:22:01 +0200
changeset 23262 0fafccb015e6
parent 23261 85f27f79232f
child 23263 0c227412b285
eliminated Code_Generator.thy
src/HOL/Tools/meson.ML
--- 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);