# HG changeset patch
# User haftmann
# Date 1216980216 -7200
# Node ID add9a605d5620cd5a80b106caf4902093ded8978
# Parent  25aceefd4786d34af4d1a801eff59b04b6e82299
dropped PureThy.note; added PureThy.add_thm

diff -r 25aceefd4786 -r add9a605d562 src/HOL/ex/Quickcheck.thy
--- 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
diff -r 25aceefd4786 -r add9a605d562 src/Pure/axclass.ML
--- 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))))
diff -r 25aceefd4786 -r add9a605d562 src/Pure/pure_thy.ML
--- 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