src/Pure/Isar/locale.ML

 
 (** store results **)
 
 (* naming of interpreted theorems *)
 
-fun global_note_prefix_i kind loc (fully_qualified, prfx) args thy =
+fun global_note_prefix_i kind loc (fully_qualified, prfx) params args thy =
   thy
   |> Sign.qualified_names
   |> Sign.add_path (NameSpace.base loc ^ "_locale")
   |> (if fully_qualified then Sign.sticky_prefix prfx else Sign.add_path prfx)
+  |> (if fully_qualified then Sign.add_path (space_implode "_" params) else I)
   |> PureThy.note_thmss kind args
   ||> Sign.restore_naming thy;
 
-fun local_note_prefix_i kind loc (fully_qualified, prfx) args ctxt =
+fun local_note_prefix_i kind loc (fully_qualified, prfx) params args ctxt =
   ctxt
   |> ProofContext.qualified_names
   |> ProofContext.add_path (NameSpace.base loc ^ "_locale")
   |> (if fully_qualified then ProofContext.sticky_prefix prfx else ProofContext.add_path prfx)
+  |> (if fully_qualified then ProofContext.add_path (space_implode "_" params) else I)
   |> ProofContext.note_thmss_i kind args
   ||> ProofContext.restore_naming ctxt;
 
 
 (* join equations of an id with already accumulated ones *)

     val morphism =
       Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
   in Element.facts_map (Element.morph_ctxt morphism) facts end;
 
 
-(* suppress application of name morphism: workaroud for class package *) (* FIXME *)
-
 fun morph_ctxt' phi = Element.map_ctxt
   {name = I,
    var = Morphism.var phi,
    typ = Morphism.typ phi,
    term = Morphism.term phi,

 (* compute morphism and apply to args *)
 
 fun interpret_args thy prfx insts prems eqns atts2 exp attrib args =
   let
     val inst = Morphism.name_morphism (NameSpace.qualified prfx) $>
+(* need to add parameter prefix *) (* FIXME *)
       Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
       Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
       Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns)
   in
     args |> Element.facts_map (morph_ctxt' inst) |>
+(* suppresses application of name morphism: workaroud for class package *) (* FIXME *)
       map (fn (attn, bs) => (attn,
         bs |> map (fn (ths, atts) => (ths, (atts @ atts2))))) |>
       standardize thy exp |> Attrib.map_facts attrib
   end;
 

     fun activate (vts, (((fully_qualified, prfx), atts2), (exp, imp), _, _)) thy =
       let
         val (insts, prems, eqns) = collect_global_witnesses thy imp parms ids vts;
         val attrib = Attrib.attribute_i thy;
         val args' = interpret_args thy prfx insts prems eqns atts2 exp attrib args;
-      in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end;
+      in global_note_prefix_i kind target (fully_qualified, prfx) (map fst parms) args' thy |> snd end;
   in fold activate regs thy end;
 
 
 (* locale results *)
 

         let
           val ctxt = mk_ctxt thy_ctxt;
           val facts' = interpret_args (ProofContext.theory_of ctxt) prfx
               (Symtab.empty, Symtab.empty) prems eqns atts
               exp (attrib thy_ctxt) facts;
-        in snd (note_interp kind loc (fully_qualified, prfx) facts' thy_ctxt) end
+        in snd (note_interp kind loc (fully_qualified, prfx) [] facts' thy_ctxt) end
       | activate_elem _ _ _ _ thy_ctxt = thy_ctxt;
 
     fun activate_elems all_eqns ((id, _), elems) thy_ctxt =
       let
         val (prfx_atts, _, _) = case get_reg thy_ctxt imp id

                     |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism)
                     |> map (apfst (apsnd (fn a => a @ map (Attrib.attribute thy) atts2)))
                     |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
                 in
                   thy
-                  |> global_note_prefix_i kind loc (fully_qualified, prfx) facts'
+                  |> global_note_prefix_i kind loc (fully_qualified, prfx) [] facts'
                   |> snd
                 end
               | activate_elem _ _ thy = thy;
 
             fun activate_elems ((id, _), elems) thy = fold (activate_elem id) elems thy;