--- a/src/HOL/ex/Quickcheck.thy Fri Jul 25 12:03:34 2008 +0200
+++ b/src/HOL/ex/Quickcheck.thy Fri Jul 25 12:03:36 2008 +0200
@@ -121,7 +121,7 @@
|> singleton (ProofContext.export lthy (ProofContext.init thy))
in
lthy
- |> LocalTheory.theory (PureThy.note Thm.internalK (fst (dest_Free random') ^ "_code", thm)
+ |> LocalTheory.theory (PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [PureThy.kind_internal])
#-> Code.add_func)
end;
in
--- a/src/Pure/axclass.ML Fri Jul 25 12:03:34 2008 +0200
+++ b/src/Pure/axclass.ML Fri Jul 25 12:03:36 2008 +0200
@@ -374,7 +374,7 @@
(Thm.def_name c', Logic.mk_equals (Const (c, T'), const'))
#>> Thm.varifyT
#-> (fn thm => add_inst_param (c, tyco) (c'', thm)
- #> PureThy.note Thm.internalK (c', thm)
+ #> PureThy.add_thm ((c', thm), [PureThy.kind_internal])
#> snd
#> Sign.restore_naming thy
#> pair (Const (c, T))))
--- a/src/Pure/pure_thy.ML Fri Jul 25 12:03:34 2008 +0200
+++ b/src/Pure/pure_thy.ML Fri Jul 25 12:03:36 2008 +0200
@@ -43,10 +43,10 @@
val store_thms: bstring * thm list -> theory -> thm list * theory
val store_thm: bstring * thm -> theory -> thm * theory
val store_thm_open: bstring * thm -> theory -> thm * theory
+ val add_thm: (bstring * thm) * attribute list -> theory -> thm * theory
val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory
val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory
val add_thms_dynamic: bstring * (Context.generic -> thm list) -> theory -> theory
- val note: string -> string * thm -> theory -> thm * theory
val note_thmss: string -> ((bstring * attribute list) *
(Facts.ref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
val note_thmss_i: string -> ((bstring * attribute list) *
@@ -228,6 +228,7 @@
val add_thmss = gen_add_thmss (name_thms true true);
val add_thms = gen_add_thms (name_thms true true);
+val add_thm = yield_singleton add_thms;
(* add_thms_dynamic *)
@@ -257,10 +258,6 @@
end;
-fun note kind (name, thm) =
- note_thmss_i kind [((name, []), [([thm], [])])]
- #>> (fn [(_, [thm])] => thm);
-
fun note_thmss_qualified k path facts thy =
thy
|> Sign.add_path path