1.1 --- a/src/Pure/Isar/locale.ML	Wed Aug 27 16:32:48 2008 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Wed Aug 27 17:54:31 2008 +0200
     1.3 @@ -1571,19 +1571,21 @@
     1.4  
     1.5  (* naming of interpreted theorems *)
     1.6  
     1.7 -fun global_note_prefix_i kind loc (fully_qualified, prfx) args thy =
     1.8 +fun global_note_prefix_i kind loc (fully_qualified, prfx) params args thy =
     1.9    thy
    1.10    |> Sign.qualified_names
    1.11    |> Sign.add_path (NameSpace.base loc ^ "_locale")
    1.12    |> (if fully_qualified then Sign.sticky_prefix prfx else Sign.add_path prfx)
    1.13 +  |> (if fully_qualified then Sign.add_path (space_implode "_" params) else I)
    1.14    |> PureThy.note_thmss kind args
    1.15    ||> Sign.restore_naming thy;
    1.16  
    1.17 -fun local_note_prefix_i kind loc (fully_qualified, prfx) args ctxt =
    1.18 +fun local_note_prefix_i kind loc (fully_qualified, prfx) params args ctxt =
    1.19    ctxt
    1.20    |> ProofContext.qualified_names
    1.21    |> ProofContext.add_path (NameSpace.base loc ^ "_locale")
    1.22    |> (if fully_qualified then ProofContext.sticky_prefix prfx else ProofContext.add_path prfx)
    1.23 +  |> (if fully_qualified then ProofContext.add_path (space_implode "_" params) else I)
    1.24    |> ProofContext.note_thmss_i kind args
    1.25    ||> ProofContext.restore_naming ctxt;
    1.26  
    1.27 @@ -1642,8 +1644,6 @@
    1.28    in Element.facts_map (Element.morph_ctxt morphism) facts end;
    1.29  
    1.30  
    1.31 -(* suppress application of name morphism: workaroud for class package *) (* FIXME *)
    1.32 -
    1.33  fun morph_ctxt' phi = Element.map_ctxt
    1.34    {name = I,
    1.35     var = Morphism.var phi,
    1.36 @@ -1658,11 +1658,13 @@
    1.37  fun interpret_args thy prfx insts prems eqns atts2 exp attrib args =
    1.38    let
    1.39      val inst = Morphism.name_morphism (NameSpace.qualified prfx) $>
    1.40 +(* need to add parameter prefix *) (* FIXME *)
    1.41        Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
    1.42        Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
    1.43        Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns)
    1.44    in
    1.45      args |> Element.facts_map (morph_ctxt' inst) |>
    1.46 +(* suppresses application of name morphism: workaroud for class package *) (* FIXME *)
    1.47        map (fn (attn, bs) => (attn,
    1.48          bs |> map (fn (ths, atts) => (ths, (atts @ atts2))))) |>
    1.49        standardize thy exp |> Attrib.map_facts attrib
    1.50 @@ -1686,7 +1688,7 @@
    1.51          val (insts, prems, eqns) = collect_global_witnesses thy imp parms ids vts;
    1.52          val attrib = Attrib.attribute_i thy;
    1.53          val args' = interpret_args thy prfx insts prems eqns atts2 exp attrib args;
    1.54 -      in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end;
    1.55 +      in global_note_prefix_i kind target (fully_qualified, prfx) (map fst parms) args' thy |> snd end;
    1.56    in fold activate regs thy end;
    1.57  
    1.58  
    1.59 @@ -2089,7 +2091,7 @@
    1.60            val facts' = interpret_args (ProofContext.theory_of ctxt) prfx
    1.61                (Symtab.empty, Symtab.empty) prems eqns atts
    1.62                exp (attrib thy_ctxt) facts;
    1.63 -        in snd (note_interp kind loc (fully_qualified, prfx) facts' thy_ctxt) end
    1.64 +        in snd (note_interp kind loc (fully_qualified, prfx) [] facts' thy_ctxt) end
    1.65        | activate_elem _ _ _ _ thy_ctxt = thy_ctxt;
    1.66  
    1.67      fun activate_elems all_eqns ((id, _), elems) thy_ctxt =
    1.68 @@ -2376,7 +2378,7 @@
    1.69                      |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
    1.70                  in
    1.71                    thy
    1.72 -                  |> global_note_prefix_i kind loc (fully_qualified, prfx) facts'
    1.73 +                  |> global_note_prefix_i kind loc (fully_qualified, prfx) [] facts'
    1.74                    |> snd
    1.75                  end
    1.76                | activate_elem _ _ thy = thy;