# HG changeset patch
# User wenzelm
# Date 911209360 -3600
# Node ID 2c037ffa728755490b37522464f8d0dd31416ef1
# Parent  5d4fc952be47a110b8991c178eba1fd0c1e96c0d
Attribute.thms_of;

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;