Interpretation commands no longer accept interpretation attributes.

--- a/NEWS	Tue Sep 02 16:55:33 2008 +0200
+++ b/NEWS	Tue Sep 02 17:31:20 2008 +0200
@@ -24,10 +24,13 @@
 
 * Dropped "locale (open)".  INCOMPATBILITY.
 
-* Command 'interpretation' no longer attempts to simplify goal.
+* Interpretation commands no longer attempt to simplify goal.
 INCOMPATIBILITY: in rare situations the generated goal differs.  Use
 methods intro_locales and unfold_locales to clarify.
 
+* Interpretation commands no longer accept interpretation attributes.
+INCOMPATBILITY.
+
 * Command 'instance': attached definitions no longer accepted.
 INCOMPATIBILITY, use proper 'instantiation' target.
 

--- a/doc-src/IsarRef/Thy/Spec.thy	Tue Sep 02 16:55:33 2008 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Tue Sep 02 17:31:20 2008 +0200
@@ -468,7 +468,7 @@
     ;
     instantiation: ('[' (inst+) ']')?
     ;
-    interp: thmdecl? \\ (contextexpr instantiation |
+    interp: (name ':')? \\ (contextexpr instantiation |
       name instantiation 'where' (thmdecl? prop + 'and'))
     ;
   \end{rail}
@@ -497,18 +497,18 @@
   restricted to a locale name.
 
   The command is aware of interpretations already active in the
-  theory.  No proof obligations are generated for those, neither is
-  post-processing applied to their facts.  This avoids duplication of
-  interpreted facts, in particular.  Note that, in the case of a
-  locale with import, parts of the interpretation may already be
-  active.  The command will only generate proof obligations and
-  process facts for new parts.
+  theory, but does not simplify the goal automatically.  In order to
+  simplify the proof obligations use methods @{method intro_locales}
+  or @{method unfold_locales}.  Post-processing is not applied to
+  facts of interpretations that are already active.  This avoids
+  duplication of interpreted facts, in particular.  Note that, in the
+  case of a locale with import, parts of the interpretation may
+  already be active.  The command will only process facts for new
+  parts.
 
-  The context expression may be preceded by a name and/or attributes.
-  These take effect in the post-processing of facts.  The name is used
-  to prefix fact names, for example to avoid accidental hiding of
-  other facts.  Attributes are applied after attributes of the
-  interpreted facts.
+  The context expression may be preceded by a name, which takes effect
+  in the post-processing of facts.  It is used to prefix fact names,
+  for example to avoid accidental hiding of other facts.
 
   Adding facts to locales has the effect of adding interpreted facts
   to the theory for all active interpretations also.  That is,

--- a/doc-src/IsarRef/Thy/document/Spec.tex	Tue Sep 02 16:55:33 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Tue Sep 02 17:31:20 2008 +0200
@@ -481,7 +481,7 @@
     ;
     instantiation: ('[' (inst+) ']')?
     ;
-    interp: thmdecl? \\ (contextexpr instantiation |
+    interp: (name ':')? \\ (contextexpr instantiation |
       name instantiation 'where' (thmdecl? prop + 'and'))
     ;
   \end{rail}
@@ -509,18 +509,18 @@
   restricted to a locale name.
 
   The command is aware of interpretations already active in the
-  theory.  No proof obligations are generated for those, neither is
-  post-processing applied to their facts.  This avoids duplication of
-  interpreted facts, in particular.  Note that, in the case of a
-  locale with import, parts of the interpretation may already be
-  active.  The command will only generate proof obligations and
-  process facts for new parts.
+  theory, but does not simplify the goal automatically.  In order to
+  simplify the proof obligations use methods \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}
+  or \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}.  Post-processing is not applied to
+  facts of interpretations that are already active.  This avoids
+  duplication of interpreted facts, in particular.  Note that, in the
+  case of a locale with import, parts of the interpretation may
+  already be active.  The command will only process facts for new
+  parts.
 
-  The context expression may be preceded by a name and/or attributes.
-  These take effect in the post-processing of facts.  The name is used
-  to prefix fact names, for example to avoid accidental hiding of
-  other facts.  Attributes are applied after attributes of the
-  interpreted facts.
+  The context expression may be preceded by a name, which takes effect
+  in the post-processing of facts.  It is used to prefix fact names,
+  for example to avoid accidental hiding of other facts.
 
   Adding facts to locales has the effect of adding interpreted facts
   to the theory for all active interpretations also.  That is,

--- a/src/FOL/ex/LocaleTest.thy	Tue Sep 02 16:55:33 2008 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Tue Sep 02 17:31:20 2008 +0200
@@ -82,12 +82,12 @@
 locale IL
 locale IM = fixes a and b and c
 
-interpretation test [simp]: IL + IM a b c [x y z] .
+interpretation test: IL + IM a b c [x y z] .
 
 print_interps IL    (* output: test *)
 print_interps IM    (* output: test *)
 
-interpretation test [simp]: IL print_interps IM .
+interpretation test: IL print_interps IM .
 
 interpretation IL .
 
@@ -252,12 +252,6 @@
 
 locale IL11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]]
 
-lemma "[| P; Q |] ==> P & Q"
-proof -
-  interpret [intro]: IL11 .     txt {* Attribute supplied at instantiation. *}
-  assume Q and P
-  then show "P & Q" ..
-qed
 
 subsection {* Simple locale with assumptions *}
 

--- a/src/HOL/Algebra/IntRing.thy	Tue Sep 02 16:55:33 2008 +0200
+++ b/src/HOL/Algebra/IntRing.thy	Tue Sep 02 17:31:20 2008 +0200
@@ -204,7 +204,7 @@
   "(True ==> PROP R) == PROP R"
   by simp_all
 
-interpretation int [unfolded UNIV]:
+interpretation int (* FIXME [unfolded UNIV] *) :
   partial_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
   where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
     and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
@@ -220,7 +220,7 @@
     by (simp add: lless_def) auto
 qed
 
-interpretation int [unfolded UNIV]:
+interpretation int (* FIXME [unfolded UNIV] *) :
   lattice ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
   where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
     and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
@@ -246,7 +246,7 @@
     done
 qed
 
-interpretation int [unfolded UNIV]:
+interpretation int (* [unfolded UNIV] *) :
   total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
   by unfold_locales clarsimp
 

--- a/src/Pure/Isar/class.ML	Tue Sep 02 16:55:33 2008 +0200
+++ b/src/Pure/Isar/class.ML	Tue Sep 02 17:31:20 2008 +0200
@@ -373,7 +373,7 @@
   in
     thy
     |> fold2 add_constraint (map snd consts) no_constraints
-    |> prove_interpretation tac ((false, prfx), []) (Locale.Locale class)
+    |> prove_interpretation tac (false, prfx) (Locale.Locale class)
           (inst, map (fn def => (Attrib.no_binding, def)) defs)
     |> fold2 add_constraint (map snd consts) constraints
   end;

--- a/src/Pure/Isar/isar_syn.ML	Tue Sep 02 16:55:33 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 02 17:31:20 2008 +0200
@@ -390,24 +390,26 @@
           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
             (Locale.add_locale "" name expr elems #-> TheoryTarget.begin)));
 
+val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Name.no_binding;
+
 val _ =
   OuterSyntax.command "interpretation"
     "prove and register interpretation of locale expression in theory or locale" K.thy_goal
     (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr
       >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) ||
-      SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
-        >> (fn (((name, atts), expr), insts) => Toplevel.print o
+      opt_prefix  -- SpecParse.locale_expr -- SpecParse.locale_insts
+        >> (fn ((name, expr), insts) => Toplevel.print o
             Toplevel.theory_to_proof
-              (Locale.interpretation I ((true, Name.name_of name), atts) expr insts)));
+              (Locale.interpretation I (true, Name.name_of name) expr insts)));
 
 val _ =
   OuterSyntax.command "interpret"
     "prove and register interpretation of locale expression in proof context"
     (K.tag_proof K.prf_goal)
-    (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
-      >> (fn (((name, atts), expr), insts) => Toplevel.print o
+    (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
+      >> (fn ((name, expr), insts) => Toplevel.print o
           Toplevel.proof'
-            (Locale.interpret Seq.single ((true, Name.name_of name), atts) expr insts)));
+            (Locale.interpret Seq.single (true, Name.name_of name) expr insts)));
 
 
 (* classes *)

--- a/src/Pure/Isar/locale.ML	Tue Sep 02 16:55:33 2008 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Sep 02 17:31:20 2008 +0200
@@ -97,21 +97,21 @@
   val add_declaration: string -> declaration -> Proof.context -> Proof.context
 
   val interpretation_i: (Proof.context -> Proof.context) ->
-    (bool * string) * Attrib.src list -> expr ->
+    bool * string -> expr ->
     term option list * (Attrib.binding * term) list ->
     theory -> Proof.state
   val interpretation: (Proof.context -> Proof.context) ->
-    (bool * string) * Attrib.src list -> expr ->
+    bool * string -> expr ->
     string option list * (Attrib.binding * string) list ->
     theory -> Proof.state
   val interpretation_in_locale: (Proof.context -> Proof.context) ->
     xstring * expr -> theory -> Proof.state
   val interpret_i: (Proof.state -> Proof.state Seq.seq) ->
-    (bool * string) * Attrib.src list -> expr ->
+    bool * string -> expr ->
     term option list * (Attrib.binding * term) list ->
     bool -> Proof.state -> Proof.state
   val interpret: (Proof.state -> Proof.state Seq.seq) ->
-    (bool * string) * Attrib.src list -> expr ->
+    bool * string -> expr ->
     string option list * (Attrib.binding * string) list ->
     bool -> Proof.state -> Proof.state
 end;
@@ -202,7 +202,7 @@
 (** management of registrations in theories and proof contexts **)
 
 type registration =
-  {attn: (bool * string) * Attrib.src list,
+  {prfx: bool * string,
       (* parameters and prefix
        (if the Boolean flag is set, only accesses containing the prefix are generated,
         otherwise the prefix may be omitted when accessing theorems etc.) *)
@@ -223,20 +223,18 @@
     val join: T * T -> T
     val dest: theory -> T ->
       (term list *
-        (((bool * string) * Attrib.src list) *
+        ((bool * string) *
          (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) *
          Element.witness list *
          thm Termtab.table)) list
     val test: theory -> T * term list -> bool
     val lookup: theory ->
       T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
-      (((bool * string) * Attrib.src list) *
-        Element.witness list *
-        thm Termtab.table) option
-    val insert: theory -> term list -> ((bool * string) * Attrib.src list) ->
+      ((bool * string) * Element.witness list * thm Termtab.table) option
+    val insert: theory -> term list -> (bool * string) ->
       (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
       T ->
-      T * (term list * (((bool * string) * Attrib.src list) * Element.witness list)) list
+      T * (term list * ((bool * string) * Element.witness list)) list
     val add_witness: term list -> Element.witness -> T -> T
     val add_equation: term list -> thm -> T -> T
   end =
@@ -245,14 +243,14 @@
      NB: index is exported whereas content is internalised. *)
   type T = registration Termtab.table;
 
-  fun mk_reg attn exp imp wits eqns =
-    {attn = attn, exp = exp, imp = imp, wits = wits, eqns = eqns};
+  fun mk_reg prfx exp imp wits eqns =
+    {prfx = prfx, exp = exp, imp = imp, wits = wits, eqns = eqns};
 
   fun map_reg f reg =
     let
-      val {attn, exp, imp, wits, eqns} = reg;
-      val (attn', exp', imp', wits', eqns') = f (attn, exp, imp, wits, eqns);
-    in mk_reg attn' exp' imp' wits' eqns' end;
+      val {prfx, exp, imp, wits, eqns} = reg;
+      val (prfx', exp', imp', wits', eqns') = f (prfx, exp, imp, wits, eqns);
+    in mk_reg prfx' exp' imp' wits' eqns' end;
 
   val empty = Termtab.empty;
 
@@ -265,11 +263,11 @@
     in ut t [] end;
 
   (* joining of registrations:
-     - prefix, attributes and morphisms of right theory;
+     - prefix and morphisms of right theory;
      - witnesses are equal, no attempt to subsumption testing;
      - union of equalities, if conflicting (i.e. two eqns with equal lhs)
        eqn of right theory takes precedence *)
-  fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {attn = n, exp, imp, wits = w, eqns = e2}) =>
+  fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {prfx = n, exp, imp, wits = w, eqns = e2}) =>
       mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2))) (r1, r2);
 
   fun dest_transfer thy regs =
@@ -277,7 +275,7 @@
       (n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es))));
 
   fun dest thy regs = dest_transfer thy regs |> map (apfst untermify) |>
-    map (apsnd (fn {attn, exp, imp, wits, eqns} => (attn, (exp, imp), wits, eqns)));
+    map (apsnd (fn {prfx, exp, imp, wits, eqns} => (prfx, (exp, imp), wits, eqns)));
 
   (* registrations that subsume t *)
   fun subsumers thy t regs =
@@ -295,7 +293,7 @@
     in
       (case subs of
         [] => NONE
-        | ((t', {attn = (prfx, atts), exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns}) :: _) =>
+        | ((t', {prfx, exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns}) :: _) =>
           let
             val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
             val tinst' = domT' |> map (fn (T as TFree (x, _)) =>
@@ -305,7 +303,7 @@
                 (x, t |> Morphism.term exp' |> Envir.subst_vars (tinst, inst)
                       |> var_inst_term (impT, imp))) |> Symtab.make;
             val inst'_morph = Element.inst_morphism thy (tinst', inst');
-          in SOME ((prfx, map (Args.morph_values inst'_morph) atts),
+          in SOME (prfx,
             map (Element.morph_witness inst'_morph) wits,
             Termtab.map (Morphism.thm inst'_morph) eqns)
           end)
@@ -313,7 +311,7 @@
 
   (* add registration if not subsumed by ones already present,
      additionally returns registrations that are strictly subsumed *)
-  fun insert thy ts attn (exp, imp) regs =
+  fun insert thy ts prfx (exp, imp) regs =
     let
       val t = termify ts;
       val subs = subsumers thy t regs ;
@@ -321,8 +319,8 @@
         [] => let
                 val sups =
                   filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs);
-                val sups' = map (apfst untermify) sups |> map (fn (ts, {attn, wits, ...}) => (ts, (attn, wits)))
-              in (Termtab.update (t, mk_reg attn exp imp [] Termtab.empty) regs, sups') end
+                val sups' = map (apfst untermify) sups |> map (fn (ts, {prfx, wits, ...}) => (ts, (prfx, wits)))
+              in (Termtab.update (t, mk_reg prfx exp imp [] Termtab.empty) regs, sups') end
       | _ => (regs, []))
     end;
 
@@ -458,24 +456,24 @@
 
 (* add registration to theory or context, ignored if subsumed *)
 
-fun put_registration (name, ps) attn morphs (* wits *) ctxt =
+fun put_registration (name, ps) prfx morphs (* wits *) ctxt =
   RegistrationsData.map (fn regs =>
     let
       val thy = Context.theory_of ctxt;
       val reg = the_default Registrations.empty (Symtab.lookup regs name);
-      val (reg', sups) = Registrations.insert thy ps attn morphs (* wits *) reg;
+      val (reg', sups) = Registrations.insert thy ps prfx morphs (* wits *) reg;
       val _ = if not (null sups) then warning
                 ("Subsumed interpretation(s) of locale " ^
                  quote (extern thy name) ^
                  "\nwith the following prefix(es):" ^
-                  commas_quote (map (fn (_, (((_, s), _), _)) => s) sups))
+                  commas_quote (map (fn (_, ((_, s), _)) => s) sups))
               else ();
     in Symtab.update (name, reg') regs end) ctxt;
 
-fun put_global_registration id attn morphs =
-  Context.theory_map (put_registration id attn morphs);
-fun put_local_registration id attn morphs =
-  Context.proof_map (put_registration id attn morphs);
+fun put_global_registration id prfx morphs =
+  Context.theory_map (put_registration id prfx morphs);
+fun put_local_registration id prfx morphs =
+  Context.proof_map (put_registration id prfx morphs);
 
 
 fun put_registration_in_locale name id =
@@ -522,11 +520,8 @@
     val prt_thm = prt_term o prop_of;
     fun prt_inst ts =
         Pretty.enclose "(" ")" (Pretty.breaks (map prt_term' ts));
-    fun prt_attn ((false, prfx), atts) =
-        Pretty.breaks (Pretty.str prfx :: Pretty.str "(optional)" ::
-          Attrib.pretty_attribs ctxt atts)
-      | prt_attn ((true, prfx), atts) =
-        Pretty.breaks (Pretty.str prfx :: Attrib.pretty_attribs ctxt atts);
+    fun prt_prfx (false, prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str "(optional)"]
+      | prt_prfx (true, prfx) = [Pretty.str prfx];
     fun prt_eqns [] = Pretty.str "no equations."
       | prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 ::
           Pretty.breaks (map prt_thm eqns));
@@ -535,15 +530,15 @@
     fun prt_witns [] = Pretty.str "no witnesses."
       | prt_witns witns = Pretty.block (Pretty.str "witnesses:" :: Pretty.brk 1 ::
           Pretty.breaks (map (Element.pretty_witness ctxt) witns))
-    fun prt_reg (ts, (((_, ""), []), _, witns, eqns)) =
+    fun prt_reg (ts, ((_, ""), _, witns, eqns)) =
         if show_wits
           then Pretty.block (prt_core ts eqns @ [Pretty.fbrk, prt_witns witns])
           else Pretty.block (prt_core ts eqns)
-      | prt_reg (ts, (attn, _, witns, eqns)) =
+      | prt_reg (ts, (prfx, _, witns, eqns)) =
         if show_wits
-          then Pretty.block ((prt_attn attn @ [Pretty.str ":", Pretty.brk 1] @
+          then Pretty.block ((prt_prfx prfx @ [Pretty.str ":", Pretty.brk 1] @
             prt_core ts eqns @ [Pretty.fbrk, prt_witns witns]))
-          else Pretty.block ((prt_attn attn @
+          else Pretty.block ((prt_prfx prfx @
             [Pretty.str ":", Pretty.brk 1] @ prt_core ts eqns));
 
     val loc_int = intern thy loc;
@@ -554,7 +549,7 @@
         NONE => Pretty.str ("no interpretations")
       | SOME r => let
             val r' = Registrations.dest thy r;
-            val r'' = Library.sort_wrt (fn (_, (((_, prfx), _), _, _, _)) => prfx) r';
+            val r'' = Library.sort_wrt (fn (_, ((_, prfx), _, _, _)) => prfx) r';
           in Pretty.big_list ("interpretations:") (map prt_reg r'') end)
     |> Pretty.writeln
   end;
@@ -996,7 +991,7 @@
               val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
             in if test_local_registration ctxt' (name, ps') then ctxt'
               else let
-                  val ctxt'' = put_local_registration (name, ps') ((true, ""), [])
+                  val ctxt'' = put_local_registration (name, ps') (true, "")
                     (Morphism.identity, ((Vartab.empty, []), (Vartab.empty, []) )) ctxt'
                 in case mode of
                     Assumed axs =>
@@ -1652,7 +1647,7 @@
 
 (* compute morphism and apply to args *)
 
-fun interpret_args thy prfx insts prems eqns atts2 exp attrib args =
+fun interpret_args thy prfx insts prems eqns exp attrib args =
   let
     val inst = Morphism.name_morphism (Name.map_name (NameSpace.qualified prfx)) $>
 (* need to add parameter prefix *) (* FIXME *)
@@ -1662,8 +1657,6 @@
   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;
 
@@ -1680,12 +1673,12 @@
     val regs = get_global_registrations thy target;
     (* add args to thy for all registrations *)
 
-    fun activate (vts, (((fully_qualified, prfx), atts2), (exp, imp), _, _)) thy =
+    fun activate (vts, ((fully_qualified, prfx), (exp, imp), _, _)) thy =
       let
         val (insts, prems, eqns) = collect_global_witnesses thy imp parms ids vts;
         val attrib = Attrib.attribute_i thy;
         val args' = args
-          |> interpret_args thy prfx insts prems eqns atts2 exp attrib
+          |> interpret_args thy prfx insts prems eqns exp attrib
           |> add_param_prefixss (space_implode "_" (map fst parms));
       in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end;
   in fold activate regs thy end;
@@ -2059,7 +2052,7 @@
     val ord = prod_ord string_ord (list_ord Term.fast_term_ord));
 
 fun gen_activate_facts_elemss mk_ctxt get_reg note note_interp attrib put_reg test_reg add_wit add_eqn
-        attn all_elemss propss eq_attns (exp, imp) thmss thy_ctxt =
+        prfx all_elemss propss eq_attns (exp, imp) thmss thy_ctxt =
   let
     val ctxt = mk_ctxt thy_ctxt;
     val (all_propss, eq_props) = chop (length all_elemss) propss;
@@ -2073,8 +2066,8 @@
 
     val thy_ctxt' = thy_ctxt
       (* add registrations *)
-(*      |> fold (fn ((id, _), _) => put_reg id attn (exp, imp)) new_elemss *)
-      |> fold (fn (id, _) => put_reg id attn (exp, imp)) new_propss
+(*      |> fold (fn ((id, _), _) => put_reg id prfx (exp, imp)) new_elemss *)
+      |> fold (fn (id, _) => put_reg id prfx (exp, imp)) new_propss
       (* add witnesses of Assumed elements (only those generate proof obligations) *)
       |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst new_propss ~~ new_thmss)
       (* add equations *)
@@ -2086,22 +2079,21 @@
           (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id)
             | ((_, Derived _), _) => NONE) all_elemss);
 
-    fun activate_elem eqns loc ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt =
+    fun activate_elem eqns loc (fully_qualified, prfx) (Notes (kind, facts)) thy_ctxt =
         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;
+              (Symtab.empty, Symtab.empty) prems eqns exp (attrib thy_ctxt) facts;
         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
+        val (prfx, _, _) = case get_reg thy_ctxt imp id
          of SOME x => x
           | NONE => sys_error ("Unknown registration of " ^ quote (fst id)
               ^ " while activating facts.");
-      in fold (activate_elem (the (Idtab.lookup all_eqns id)) (fst id) prfx_atts) elems thy_ctxt end;
+      in fold (activate_elem (the (Idtab.lookup all_eqns id)) (fst id) prfx) elems thy_ctxt end;
 
     val thy_ctxt'' = thy_ctxt'
       (* add witnesses of Derived elements *)
@@ -2209,7 +2201,7 @@
 
 fun gen_prep_registration mk_ctxt test_reg activate
     prep_attr prep_expr prep_insts
-    thy_ctxt raw_attn raw_expr raw_insts =
+    thy_ctxt prfx raw_expr raw_insts =
   let
     val ctxt = mk_ctxt thy_ctxt;
     val thy = ProofContext.theory_of ctxt;
@@ -2217,7 +2209,6 @@
     fun prep_attn attn = (apsnd o map)
       (Attrib.crude_closure ctxt o Args.assignable o prep_attr thy) attn;
 
-    val attn = prep_attn raw_attn;
     val expr = prep_expr thy raw_expr;
 
     val pts = params_of_expr ctxt' [] expr ([], Symtab.empty, Symtab.empty);
@@ -2274,7 +2265,7 @@
 
     val propss = map extract_asms_elems inst_elemss @ eqn_elems;
 
-  in (propss, activate attn inst_elemss propss eq_attns morphs) end;
+  in (propss, activate prfx inst_elemss propss eq_attns morphs) end;
 
 fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init
   test_global_registration
@@ -2333,7 +2324,7 @@
                 |> fold (add_witness_in_locale target id) thms
           | activate_id _ thy = thy;
 
-        fun activate_reg (vts, (((fully_qualified, prfx), atts2), (exp, imp), _, _)) thy =
+        fun activate_reg (vts, ((fully_qualified, prfx), (exp, imp), _, _)) thy =
           let
             val (insts, wits, _) = collect_global_witnesses thy imp fixed target_ids vts;
             fun inst_parms ps = map
@@ -2348,7 +2339,7 @@
                 if test_global_registration thy (name, ps')
                 then thy
                 else thy
-                  |> put_global_registration (name, ps') ((fully_qualified, prfx), atts2) (exp, imp)
+                  |> put_global_registration (name, ps') (fully_qualified, prfx) (exp, imp)
                   |> fold (fn witn => fn thy => add_global_witness (name, ps')
                      (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms
               end;
@@ -2360,7 +2351,7 @@
                 if test_global_registration thy (name, ps')
                 then thy
                 else thy
-                  |> put_global_registration (name, ps') ((fully_qualified, prfx), atts2) (exp, imp)
+                  |> put_global_registration (name, ps') (fully_qualified, prfx) (exp, imp)
                   |> fold (fn witn => fn thy => add_global_witness (name, ps')
                        (witn |> Element.map_witness (fn (t, th) =>  (* FIXME *)
                        (Element.inst_term insts t,
@@ -2376,7 +2367,6 @@
                     Morphism.thm_morphism disch;
                   val facts' = facts
                     |> 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
@@ -2403,10 +2393,10 @@
 fun prep_result propps thmss =
   ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss);
 
-fun gen_interpretation prep_registration after_qed (prfx, raw_atts) raw_expr raw_insts thy =
+fun gen_interpretation prep_registration after_qed prfx raw_expr raw_insts thy =
   (* prfx = (flag indicating full qualification, name prefix) *)
   let
-    val (propss, activate) = prep_registration thy (prfx, raw_atts) raw_expr raw_insts;
+    val (propss, activate) = prep_registration thy prfx raw_expr raw_insts;
     fun after_qed' results =
       ProofContext.theory (activate (prep_result propss results))
       #> after_qed;
@@ -2418,12 +2408,12 @@
     |> Seq.hd
   end;
 
-fun gen_interpret prep_registration after_qed (prfx, atts) expr insts int state =
+fun gen_interpret prep_registration after_qed prfx expr insts int state =
   (* prfx = (flag indicating full qualification, name prefix) *)
   let
     val _ = Proof.assert_forward_or_chain state;
     val ctxt = Proof.context_of state;
-    val (propss, activate) = prep_registration ctxt (prfx, atts) expr insts;
+    val (propss, activate) = prep_registration ctxt prfx expr insts;
     fun after_qed' results =
       Proof.map_context (K (ctxt |> activate (prep_result propss results)))
       #> Proof.put_facts NONE