# HG changeset patch
# User ballarin
# Date 1226667652 -3600
# Node ID 4493633ab4016babbe6fff30bb31efd850518344
# Parent  bb7a102e2f5db1b914227c1ecc7f8da4cd160520
Made local_note_prefix public.

diff -r bb7a102e2f5d -r 4493633ab401 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Nov 14 08:50:11 2008 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Nov 14 14:00:52 2008 +0100
@@ -91,6 +91,9 @@
   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
 
   (* Storing results *)
+  val local_note_prefix: string ->
+    (Name.binding * attribute list) * (thm list * attribute list) list ->
+    Proof.context -> (string * thm list) * Proof.context
   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