1.1 --- a/src/Pure/pure_thy.ML	Mon Aug 17 16:02:21 1998 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Mon Aug 17 20:32:24 1998 +0200
     1.3 @@ -26,6 +26,7 @@
     1.4    val thms_closure: theory -> xstring -> tthm list option
     1.5    val get_tthm: theory -> xstring -> tthm
     1.6    val get_tthms: theory -> xstring -> tthm list
     1.7 +  val get_tthmss: theory -> xstring list -> tthm list
     1.8    val thms_containing: theory -> string list -> (string * thm) list
     1.9    val store_tthm: (bstring * tthm) * theory attribute list -> theory -> theory * tthm
    1.10    val smart_store_thm: (bstring * thm) -> thm
    1.11 @@ -131,6 +132,8 @@
    1.12      [thm] => thm
    1.13    | _ => raise THEORY ("Single theorem expected " ^ quote name, [thy]));
    1.14  
    1.15 +fun get_tthmss thy names = flat (map (get_tthms thy) names);
    1.16 +
    1.17  fun get_thms thy = map Attribute.thm_of o get_tthms thy;
    1.18  fun get_thm thy = Attribute.thm_of o get_tthm thy;
    1.19