# HG changeset patch
# User ballarin
# Date 1228314406 -3600
# Node ID b2db06eb214d597cea39c7f0c1bc73d4f47b2e57
# Parent  610fe33ca358f91174c4e65924bc16c161d430e5
Made global_note_qualified public.

diff -r 610fe33ca358 -r b2db06eb214d src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Dec 03 14:02:24 2008 +0000
+++ b/src/Pure/Isar/locale.ML	Wed Dec 03 15:26:46 2008 +0100
@@ -91,6 +91,9 @@
   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
 
   (* Storing results *)
+  val global_note_qualified: string ->
+    ((Name.binding * attribute list) * (thm list * attribute list) list) list ->
+    theory -> (string * thm list) list * theory
   val local_note_qualified: string ->
     ((Name.binding * attribute list) * (thm list * attribute list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
@@ -2409,7 +2412,6 @@
   ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss);
 
 fun gen_interpretation prep_registration after_qed prfx raw_expr raw_insts thy =
-  (* prfx = (flag indicating full qualification, name prefix) *)
   let
     val (propss, activate, morphs) = prep_registration thy prfx raw_expr raw_insts;
     fun after_qed' results =