src/Pure/thm.ML
changeset 18418 bf448d999b7e
parent 18184 43c4589a9a78
child 18486 bf8637d9d53b
     1.1 --- a/src/Pure/thm.ML	Thu Dec 15 21:51:31 2005 +0100
     1.2 +++ b/src/Pure/thm.ML	Fri Dec 16 09:00:11 2005 +0100
     1.3 @@ -142,8 +142,8 @@
     1.4    val no_prems: thm -> bool
     1.5    val no_attributes: 'a -> 'a * 'b list
     1.6    val simple_fact: 'a -> ('a * 'b list) list
     1.7 -  val apply_attributes: ('a * thm) * 'a attribute list -> 'a * thm
     1.8 -  val applys_attributes: ('a * thm list) * 'a attribute list -> 'a * thm list
     1.9 +  val apply_attributes: 'a attribute list -> 'a * thm -> 'a * thm
    1.10 +  val applys_attributes: 'a attribute list -> 'a * thm list -> 'a * thm list
    1.11    val terms_of_tpairs: (term * term) list -> term list
    1.12    val full_prop_of: thm -> term
    1.13    val get_name_tags: thm -> string * tag list
    1.14 @@ -400,8 +400,8 @@
    1.15  
    1.16  fun no_attributes x = (x, []);
    1.17  fun simple_fact x = [(x, [])];
    1.18 -fun apply_attributes (x_th, atts) = Library.apply atts x_th;
    1.19 -fun applys_attributes (x_ths, atts) = foldl_map (Library.apply atts) x_ths;
    1.20 +val apply_attributes = Library.apply;
    1.21 +fun applys_attributes atts = foldl_map (Library.apply atts);
    1.22  
    1.23  
    1.24  (* hyps *)