src/Pure/Isar/locale.ML
changeset 28950 b2db06eb214d
parent 28941 128459bd72d2
child 28965 1de908189869
     1.1 --- a/src/Pure/Isar/locale.ML	Wed Dec 03 14:02:24 2008 +0000
     1.2 +++ b/src/Pure/Isar/locale.ML	Wed Dec 03 15:26:46 2008 +0100
     1.3 @@ -91,6 +91,9 @@
     1.4    val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
     1.5  
     1.6    (* Storing results *)
     1.7 +  val global_note_qualified: string ->
     1.8 +    ((Name.binding * attribute list) * (thm list * attribute list) list) list ->
     1.9 +    theory -> (string * thm list) list * theory
    1.10    val local_note_qualified: string ->
    1.11      ((Name.binding * attribute list) * (thm list * attribute list) list) list ->
    1.12      Proof.context -> (string * thm list) list * Proof.context
    1.13 @@ -2409,7 +2412,6 @@
    1.14    ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss);
    1.15  
    1.16  fun gen_interpretation prep_registration after_qed prfx raw_expr raw_insts thy =
    1.17 -  (* prfx = (flag indicating full qualification, name prefix) *)
    1.18    let
    1.19      val (propss, activate, morphs) = prep_registration thy prfx raw_expr raw_insts;
    1.20      fun after_qed' results =