added store_tthm;
authorwenzelm
Thu Aug 06 18:21:14 1998 +0200 (1998-08-06)
changeset 52806055775a151b
parent 5279 cba6a96f5812
child 5281 f4d16517b360
added store_tthm;
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/pure_thy.ML	Thu Aug 06 17:51:03 1998 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Thu Aug 06 18:21:14 1998 +0200
     1.3 @@ -27,6 +27,7 @@
     1.4    val get_tthm: theory -> xstring -> tthm
     1.5    val get_tthms: theory -> xstring -> tthm list
     1.6    val thms_containing: theory -> string list -> (string * thm) list
     1.7 +  val store_tthm: (bstring * tthm) * theory attribute list -> theory -> theory * tthm
     1.8    val smart_store_thm: (bstring * thm) -> thm
     1.9    val add_tthms: ((bstring * tthm) * theory attribute list) list -> theory -> theory
    1.10    val add_tthmss: ((bstring * tthm list) * theory attribute list) list -> theory -> theory
    1.11 @@ -244,11 +245,22 @@
    1.12  (* add_tthms(s) *)
    1.13  
    1.14  fun add_tthmx app_name app_att ((bname, tthmx), atts) thy =
    1.15 -  let val (thy', tthmx') = app_att ((thy, tthmx), atts)
    1.16 -  in enter_tthmx (Theory.sign_of thy') app_name (bname, tthmx'); thy' end;
    1.17 +  let
    1.18 +    val (thy', tthmx') = app_att ((thy, tthmx), atts);
    1.19 +    val tthms'' = enter_tthmx (Theory.sign_of thy') app_name (bname, tthmx');
    1.20 +  in (thy', tthms'') end;
    1.21  
    1.22 -val add_tthms = Theory.apply o map (add_tthmx name_single Attribute.apply);
    1.23 -val add_tthmss = Theory.apply o map (add_tthmx name_multi Attribute.applys);
    1.24 +val add_tthms =
    1.25 +  Theory.apply o map (fn th_atts => fst o add_tthmx name_single Attribute.apply th_atts);
    1.26 +val add_tthmss =
    1.27 +  Theory.apply o map (fn th_atts => fst o add_tthmx name_multi Attribute.applys th_atts);
    1.28 +
    1.29 +
    1.30 +(* store_tthm *)
    1.31 +
    1.32 +fun store_tthm th_atts thy =
    1.33 +  let val (thy', [th']) = add_tthmx name_single Attribute.apply th_atts thy
    1.34 +  in (thy', th') end;
    1.35  
    1.36  
    1.37  (* smart_store_thm *)