Attribute.thms_of;
authorwenzelm
Mon, 16 Nov 1998 10:42:40 +0100
changeset 5871 2c037ffa7287
parent 5870 5d4fc952be47
child 5872 df19e1de5c8a
Attribute.thms_of;
src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Mon Nov 16 10:41:27 1998 +0100
+++ b/src/Pure/pure_thy.ML	Mon Nov 16 10:42:40 1998 +0100
@@ -134,7 +134,7 @@
 
 fun get_tthmss thy names = flat (map (get_tthms thy) names);
 
-fun get_thms thy = map Attribute.thm_of o get_tthms thy;
+fun get_thms thy = Attribute.thms_of o get_tthms thy;
 fun get_thm thy = Attribute.thm_of o get_tthm thy;