# HG changeset patch
# User ballarin
# Date 1226997644 -3600
# Node ID f356687a76593a2fd052324b7af099a3e216e00c
# Parent  cf7237498e7aa49d953c7e8fb7ed61f8821fff83
add_thmss

diff -r cf7237498e7a -r f356687a7659 src/Pure/Isar/new_locale.ML
--- a/src/Pure/Isar/new_locale.ML	Tue Nov 18 09:40:06 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Tue Nov 18 09:40:44 2008 +0100
@@ -26,10 +26,8 @@
   val declarations_of: theory -> string -> declaration list * declaration list;
 
   (* Storing results *)
-(*
-val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
+  val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
     Proof.context -> Proof.context
-*)
   val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
   val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
   val add_declaration: string -> declaration -> Proof.context -> Proof.context
@@ -276,6 +274,19 @@
 
 (*** Storing results ***)
 
+(* Theorems *)
+
+fun add_thmss loc kind args ctxt =
+  let
+    val (([Notes args'], _), ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
+    val ctxt'' = ctxt' |> ProofContext.theory
+      (change_locale loc
+        (fn (parameters, spec, decls, notes, dependencies) =>
+          (parameters, spec, decls, (args', stamp ()) :: notes, dependencies)))
+      (* FIXME registrations *)
+  in ctxt'' end;
+
+
 (* Declarations *)
 
 local
@@ -285,12 +296,9 @@
 fun add_decls add loc decl =
   ProofContext.theory (change_locale loc
     (fn (parameters, spec, decls, notes, dependencies) =>
-      (parameters, spec, add (decl, stamp ()) decls, notes, dependencies)))
-(*
-  #>
+      (parameters, spec, add (decl, stamp ()) decls, notes, dependencies))) #>
   add_thmss loc Thm.internalK
     [((Name.no_binding, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
-*)
 
 in