dropped PureThy.note; added PureThy.add_thm
authorhaftmann
Fri Jul 25 12:03:36 2008 +0200 (2008-07-25 ago)
changeset 27683add9a605d562
parent 27682 25aceefd4786
child 27684 f45fd1159a4b
dropped PureThy.note; added PureThy.add_thm
src/HOL/ex/Quickcheck.thy
src/Pure/axclass.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/HOL/ex/Quickcheck.thy	Fri Jul 25 12:03:34 2008 +0200
     1.2 +++ b/src/HOL/ex/Quickcheck.thy	Fri Jul 25 12:03:36 2008 +0200
     1.3 @@ -121,7 +121,7 @@
     1.4                  |> singleton (ProofContext.export lthy (ProofContext.init thy))
     1.5              in
     1.6                lthy
     1.7 -              |> LocalTheory.theory (PureThy.note Thm.internalK (fst (dest_Free random') ^ "_code", thm)
     1.8 +              |> LocalTheory.theory (PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [PureThy.kind_internal])
     1.9                     #-> Code.add_func)
    1.10              end;
    1.11          in
     2.1 --- a/src/Pure/axclass.ML	Fri Jul 25 12:03:34 2008 +0200
     2.2 +++ b/src/Pure/axclass.ML	Fri Jul 25 12:03:36 2008 +0200
     2.3 @@ -374,7 +374,7 @@
     2.4            (Thm.def_name c', Logic.mk_equals (Const (c, T'), const'))
     2.5      #>> Thm.varifyT
     2.6      #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
     2.7 -    #> PureThy.note Thm.internalK (c', thm)
     2.8 +    #> PureThy.add_thm ((c', thm), [PureThy.kind_internal])
     2.9      #> snd
    2.10      #> Sign.restore_naming thy
    2.11      #> pair (Const (c, T))))
     3.1 --- a/src/Pure/pure_thy.ML	Fri Jul 25 12:03:34 2008 +0200
     3.2 +++ b/src/Pure/pure_thy.ML	Fri Jul 25 12:03:36 2008 +0200
     3.3 @@ -43,10 +43,10 @@
     3.4    val store_thms: bstring * thm list -> theory -> thm list * theory
     3.5    val store_thm: bstring * thm -> theory -> thm * theory
     3.6    val store_thm_open: bstring * thm -> theory -> thm * theory
     3.7 +  val add_thm: (bstring * thm) * attribute list -> theory -> thm * theory
     3.8    val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory
     3.9    val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory
    3.10    val add_thms_dynamic: bstring * (Context.generic -> thm list) -> theory -> theory
    3.11 -  val note: string -> string * thm -> theory -> thm * theory
    3.12    val note_thmss: string -> ((bstring * attribute list) *
    3.13      (Facts.ref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
    3.14    val note_thmss_i: string -> ((bstring * attribute list) *
    3.15 @@ -228,6 +228,7 @@
    3.16  
    3.17  val add_thmss = gen_add_thmss (name_thms true true);
    3.18  val add_thms = gen_add_thms (name_thms true true);
    3.19 +val add_thm = yield_singleton add_thms;
    3.20  
    3.21  
    3.22  (* add_thms_dynamic *)
    3.23 @@ -257,10 +258,6 @@
    3.24  
    3.25  end;
    3.26  
    3.27 -fun note kind (name, thm) =
    3.28 -  note_thmss_i kind [((name, []), [([thm], [])])]
    3.29 -  #>> (fn [(_, [thm])] => thm);
    3.30 -
    3.31  fun note_thmss_qualified k path facts thy =
    3.32    thy
    3.33    |> Sign.add_path path