diff -r 5d4fc952be47 -r 2c037ffa7287 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;