# HG changeset patch
# User ballarin
# Date 1219852471 -7200
# Node ID d1c2fa105443ec8a6d3bb42d1ec1bcbe2d87a680
# Parent  92dd3ad302b7884d1de5f3e5e5e0b3874e7eca3e
Consistent naming of theorems in interpretation.

diff -r 92dd3ad302b7 -r d1c2fa105443 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Aug 27 16:32:48 2008 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Aug 27 17:54:31 2008 +0200
@@ -1571,19 +1571,21 @@
 
 (* 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;
 
@@ -1642,8 +1644,6 @@
   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,
@@ -1658,11 +1658,13 @@
 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
@@ -1686,7 +1688,7 @@
         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;
 
 
@@ -2089,7 +2091,7 @@
           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 =
@@ -2376,7 +2378,7 @@
                     |> 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;