1.1 --- a/src/Pure/Isar/locale.ML	Thu Aug 28 22:08:02 2008 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Thu Aug 28 22:08:11 2008 +0200
     1.3 @@ -1571,22 +1571,25 @@
     1.4  
     1.5  (* naming of interpreted theorems *)
     1.6  
     1.7 -fun global_note_prefix_i kind loc (fully_qualified, prfx) params args thy =
     1.8 +fun add_param_prefixss s =
     1.9 +  (map o apfst o apfst) (NameSpace.qualified s);
    1.10 +fun drop_param_prefixss args = (map o apfst o apfst)
    1.11 +  (fn "" => "" | s => (NameSpace.implode o tl o NameSpace.explode) s) args;
    1.12 +
    1.13 +fun global_note_prefix_i kind loc (fully_qualified, prfx) args thy =
    1.14    thy
    1.15    |> Sign.qualified_names
    1.16    |> Sign.add_path (NameSpace.base loc ^ "_locale")
    1.17    |> (if fully_qualified then Sign.sticky_prefix prfx else Sign.add_path prfx)
    1.18 -  |> (if fully_qualified then Sign.add_path (space_implode "_" params) else I)
    1.19 -  |> PureThy.note_thmss kind args
    1.20 +  |> PureThy.note_thmss kind (if fully_qualified then args else drop_param_prefixss args)
    1.21    ||> Sign.restore_naming thy;
    1.22  
    1.23 -fun local_note_prefix_i kind loc (fully_qualified, prfx) params args ctxt =
    1.24 +fun local_note_prefix_i kind loc (fully_qualified, prfx) args ctxt =
    1.25    ctxt
    1.26    |> ProofContext.qualified_names
    1.27    |> ProofContext.add_path (NameSpace.base loc ^ "_locale")
    1.28    |> (if fully_qualified then ProofContext.sticky_prefix prfx else ProofContext.add_path prfx)
    1.29 -  |> (if fully_qualified then ProofContext.add_path (space_implode "_" params) else I)
    1.30 -  |> ProofContext.note_thmss_i kind args
    1.31 +  |> ProofContext.note_thmss_i kind (if fully_qualified then args else drop_param_prefixss args)
    1.32    ||> ProofContext.restore_naming ctxt;
    1.33  
    1.34  
    1.35 @@ -1687,8 +1690,10 @@
    1.36        let
    1.37          val (insts, prems, eqns) = collect_global_witnesses thy imp parms ids vts;
    1.38          val attrib = Attrib.attribute_i thy;
    1.39 -        val args' = interpret_args thy prfx insts prems eqns atts2 exp attrib args;
    1.40 -      in global_note_prefix_i kind target (fully_qualified, prfx) (map fst parms) args' thy |> snd end;
    1.41 +        val args' = args
    1.42 +          |> interpret_args thy prfx insts prems eqns atts2 exp attrib
    1.43 +          |> add_param_prefixss (space_implode "_" (map fst parms));
    1.44 +      in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end;
    1.45    in fold activate regs thy end;
    1.46  
    1.47  
    1.48 @@ -2091,7 +2096,7 @@
    1.49            val facts' = interpret_args (ProofContext.theory_of ctxt) prfx
    1.50                (Symtab.empty, Symtab.empty) prems eqns atts
    1.51                exp (attrib thy_ctxt) facts;
    1.52 -        in snd (note_interp kind loc (fully_qualified, prfx) [] facts' thy_ctxt) end
    1.53 +        in snd (note_interp kind loc (fully_qualified, prfx) facts' thy_ctxt) end
    1.54        | activate_elem _ _ _ _ thy_ctxt = thy_ctxt;
    1.55  
    1.56      fun activate_elems all_eqns ((id, _), elems) thy_ctxt =
    1.57 @@ -2266,6 +2271,7 @@
    1.58        ((n, map (Morphism.term (inst_morphism $> fst morphs)) ps),
    1.59          map (fn Int e => Element.morph_ctxt inst_morphism e) elems)
    1.60        |> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode)));
    1.61 +
    1.62      (* equations *)
    1.63      val eqn_elems = if null eqns then []
    1.64        else [(Library.last_elem inst_elemss |> fst |> fst, eqns)];
    1.65 @@ -2378,7 +2384,7 @@
    1.66                      |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
    1.67                  in
    1.68                    thy
    1.69 -                  |> global_note_prefix_i kind loc (fully_qualified, prfx) [] facts'
    1.70 +                  |> global_note_prefix_i kind loc (fully_qualified, prfx) facts'
    1.71                    |> snd
    1.72                  end
    1.73                | activate_elem _ _ thy = thy;