| changeset 5871 | 2c037ffa7287 |
| parent 5686 | 1f053d05f571 |
| child 5907 | 4b9f4e310891 |
--- 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;