# HG changeset patch
# User haftmann
# Date 1197282257 -3600
# Node ID 2f0b4544f4b3e8b3b366b43dc14f7e21d82d0cc9
# Parent  34860182b250bbf9b12839b59bbd502fbb5c120d
added simple primitive note

diff -r 34860182b250 -r 2f0b4544f4b3 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Mon Dec 10 11:24:15 2007 +0100
+++ b/src/Pure/pure_thy.ML	Mon Dec 10 11:24:17 2007 +0100
@@ -72,6 +72,7 @@
   val forall_elim_vars: int -> thm -> thm
   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 note: string -> string * thm -> theory -> thm * theory
   val note_thmss: string -> ((bstring * attribute list) *
     (thmref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
   val note_thmss_i: string -> ((bstring * attribute list) *
@@ -398,6 +399,10 @@
 
 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