Interpretation commands no longer accept interpretation attributes.
authorballarin
Tue Sep 02 17:31:20 2008 +0200 (2008-09-02)
changeset 28085914183e229e9
parent 28084 a05ca48ef263
child 28086 db584d1d2af4
Interpretation commands no longer accept interpretation attributes.
NEWS
doc-src/IsarRef/Thy/Spec.thy
doc-src/IsarRef/Thy/document/Spec.tex
src/FOL/ex/LocaleTest.thy
src/HOL/Algebra/IntRing.thy
src/Pure/Isar/class.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/locale.ML
     1.1 --- a/NEWS	Tue Sep 02 16:55:33 2008 +0200
     1.2 +++ b/NEWS	Tue Sep 02 17:31:20 2008 +0200
     1.3 @@ -24,10 +24,13 @@
     1.4  
     1.5  * Dropped "locale (open)".  INCOMPATBILITY.
     1.6  
     1.7 -* Command 'interpretation' no longer attempts to simplify goal.
     1.8 +* Interpretation commands no longer attempt to simplify goal.
     1.9  INCOMPATIBILITY: in rare situations the generated goal differs.  Use
    1.10  methods intro_locales and unfold_locales to clarify.
    1.11  
    1.12 +* Interpretation commands no longer accept interpretation attributes.
    1.13 +INCOMPATBILITY.
    1.14 +
    1.15  * Command 'instance': attached definitions no longer accepted.
    1.16  INCOMPATIBILITY, use proper 'instantiation' target.
    1.17  
     2.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Tue Sep 02 16:55:33 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Tue Sep 02 17:31:20 2008 +0200
     2.3 @@ -468,7 +468,7 @@
     2.4      ;
     2.5      instantiation: ('[' (inst+) ']')?
     2.6      ;
     2.7 -    interp: thmdecl? \\ (contextexpr instantiation |
     2.8 +    interp: (name ':')? \\ (contextexpr instantiation |
     2.9        name instantiation 'where' (thmdecl? prop + 'and'))
    2.10      ;
    2.11    \end{rail}
    2.12 @@ -497,18 +497,18 @@
    2.13    restricted to a locale name.
    2.14  
    2.15    The command is aware of interpretations already active in the
    2.16 -  theory.  No proof obligations are generated for those, neither is
    2.17 -  post-processing applied to their facts.  This avoids duplication of
    2.18 -  interpreted facts, in particular.  Note that, in the case of a
    2.19 -  locale with import, parts of the interpretation may already be
    2.20 -  active.  The command will only generate proof obligations and
    2.21 -  process facts for new parts.
    2.22 +  theory, but does not simplify the goal automatically.  In order to
    2.23 +  simplify the proof obligations use methods @{method intro_locales}
    2.24 +  or @{method unfold_locales}.  Post-processing is not applied to
    2.25 +  facts of interpretations that are already active.  This avoids
    2.26 +  duplication of interpreted facts, in particular.  Note that, in the
    2.27 +  case of a locale with import, parts of the interpretation may
    2.28 +  already be active.  The command will only process facts for new
    2.29 +  parts.
    2.30  
    2.31 -  The context expression may be preceded by a name and/or attributes.
    2.32 -  These take effect in the post-processing of facts.  The name is used
    2.33 -  to prefix fact names, for example to avoid accidental hiding of
    2.34 -  other facts.  Attributes are applied after attributes of the
    2.35 -  interpreted facts.
    2.36 +  The context expression may be preceded by a name, which takes effect
    2.37 +  in the post-processing of facts.  It is used to prefix fact names,
    2.38 +  for example to avoid accidental hiding of other facts.
    2.39  
    2.40    Adding facts to locales has the effect of adding interpreted facts
    2.41    to the theory for all active interpretations also.  That is,
     3.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Tue Sep 02 16:55:33 2008 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Tue Sep 02 17:31:20 2008 +0200
     3.3 @@ -481,7 +481,7 @@
     3.4      ;
     3.5      instantiation: ('[' (inst+) ']')?
     3.6      ;
     3.7 -    interp: thmdecl? \\ (contextexpr instantiation |
     3.8 +    interp: (name ':')? \\ (contextexpr instantiation |
     3.9        name instantiation 'where' (thmdecl? prop + 'and'))
    3.10      ;
    3.11    \end{rail}
    3.12 @@ -509,18 +509,18 @@
    3.13    restricted to a locale name.
    3.14  
    3.15    The command is aware of interpretations already active in the
    3.16 -  theory.  No proof obligations are generated for those, neither is
    3.17 -  post-processing applied to their facts.  This avoids duplication of
    3.18 -  interpreted facts, in particular.  Note that, in the case of a
    3.19 -  locale with import, parts of the interpretation may already be
    3.20 -  active.  The command will only generate proof obligations and
    3.21 -  process facts for new parts.
    3.22 +  theory, but does not simplify the goal automatically.  In order to
    3.23 +  simplify the proof obligations use methods \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}
    3.24 +  or \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}.  Post-processing is not applied to
    3.25 +  facts of interpretations that are already active.  This avoids
    3.26 +  duplication of interpreted facts, in particular.  Note that, in the
    3.27 +  case of a locale with import, parts of the interpretation may
    3.28 +  already be active.  The command will only process facts for new
    3.29 +  parts.
    3.30  
    3.31 -  The context expression may be preceded by a name and/or attributes.
    3.32 -  These take effect in the post-processing of facts.  The name is used
    3.33 -  to prefix fact names, for example to avoid accidental hiding of
    3.34 -  other facts.  Attributes are applied after attributes of the
    3.35 -  interpreted facts.
    3.36 +  The context expression may be preceded by a name, which takes effect
    3.37 +  in the post-processing of facts.  It is used to prefix fact names,
    3.38 +  for example to avoid accidental hiding of other facts.
    3.39  
    3.40    Adding facts to locales has the effect of adding interpreted facts
    3.41    to the theory for all active interpretations also.  That is,
     4.1 --- a/src/FOL/ex/LocaleTest.thy	Tue Sep 02 16:55:33 2008 +0200
     4.2 +++ b/src/FOL/ex/LocaleTest.thy	Tue Sep 02 17:31:20 2008 +0200
     4.3 @@ -82,12 +82,12 @@
     4.4  locale IL
     4.5  locale IM = fixes a and b and c
     4.6  
     4.7 -interpretation test [simp]: IL + IM a b c [x y z] .
     4.8 +interpretation test: IL + IM a b c [x y z] .
     4.9  
    4.10  print_interps IL    (* output: test *)
    4.11  print_interps IM    (* output: test *)
    4.12  
    4.13 -interpretation test [simp]: IL print_interps IM .
    4.14 +interpretation test: IL print_interps IM .
    4.15  
    4.16  interpretation IL .
    4.17  
    4.18 @@ -252,12 +252,6 @@
    4.19  
    4.20  locale IL11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]]
    4.21  
    4.22 -lemma "[| P; Q |] ==> P & Q"
    4.23 -proof -
    4.24 -  interpret [intro]: IL11 .     txt {* Attribute supplied at instantiation. *}
    4.25 -  assume Q and P
    4.26 -  then show "P & Q" ..
    4.27 -qed
    4.28  
    4.29  subsection {* Simple locale with assumptions *}
    4.30  
     5.1 --- a/src/HOL/Algebra/IntRing.thy	Tue Sep 02 16:55:33 2008 +0200
     5.2 +++ b/src/HOL/Algebra/IntRing.thy	Tue Sep 02 17:31:20 2008 +0200
     5.3 @@ -204,7 +204,7 @@
     5.4    "(True ==> PROP R) == PROP R"
     5.5    by simp_all
     5.6  
     5.7 -interpretation int [unfolded UNIV]:
     5.8 +interpretation int (* FIXME [unfolded UNIV] *) :
     5.9    partial_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
    5.10    where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
    5.11      and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
    5.12 @@ -220,7 +220,7 @@
    5.13      by (simp add: lless_def) auto
    5.14  qed
    5.15  
    5.16 -interpretation int [unfolded UNIV]:
    5.17 +interpretation int (* FIXME [unfolded UNIV] *) :
    5.18    lattice ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
    5.19    where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
    5.20      and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
    5.21 @@ -246,7 +246,7 @@
    5.22      done
    5.23  qed
    5.24  
    5.25 -interpretation int [unfolded UNIV]:
    5.26 +interpretation int (* [unfolded UNIV] *) :
    5.27    total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
    5.28    by unfold_locales clarsimp
    5.29  
     6.1 --- a/src/Pure/Isar/class.ML	Tue Sep 02 16:55:33 2008 +0200
     6.2 +++ b/src/Pure/Isar/class.ML	Tue Sep 02 17:31:20 2008 +0200
     6.3 @@ -373,7 +373,7 @@
     6.4    in
     6.5      thy
     6.6      |> fold2 add_constraint (map snd consts) no_constraints
     6.7 -    |> prove_interpretation tac ((false, prfx), []) (Locale.Locale class)
     6.8 +    |> prove_interpretation tac (false, prfx) (Locale.Locale class)
     6.9            (inst, map (fn def => (Attrib.no_binding, def)) defs)
    6.10      |> fold2 add_constraint (map snd consts) constraints
    6.11    end;
     7.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Sep 02 16:55:33 2008 +0200
     7.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 02 17:31:20 2008 +0200
     7.3 @@ -390,24 +390,26 @@
     7.4            (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
     7.5              (Locale.add_locale "" name expr elems #-> TheoryTarget.begin)));
     7.6  
     7.7 +val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Name.no_binding;
     7.8 +
     7.9  val _ =
    7.10    OuterSyntax.command "interpretation"
    7.11      "prove and register interpretation of locale expression in theory or locale" K.thy_goal
    7.12      (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr
    7.13        >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) ||
    7.14 -      SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
    7.15 -        >> (fn (((name, atts), expr), insts) => Toplevel.print o
    7.16 +      opt_prefix  -- SpecParse.locale_expr -- SpecParse.locale_insts
    7.17 +        >> (fn ((name, expr), insts) => Toplevel.print o
    7.18              Toplevel.theory_to_proof
    7.19 -              (Locale.interpretation I ((true, Name.name_of name), atts) expr insts)));
    7.20 +              (Locale.interpretation I (true, Name.name_of name) expr insts)));
    7.21  
    7.22  val _ =
    7.23    OuterSyntax.command "interpret"
    7.24      "prove and register interpretation of locale expression in proof context"
    7.25      (K.tag_proof K.prf_goal)
    7.26 -    (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
    7.27 -      >> (fn (((name, atts), expr), insts) => Toplevel.print o
    7.28 +    (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
    7.29 +      >> (fn ((name, expr), insts) => Toplevel.print o
    7.30            Toplevel.proof'
    7.31 -            (Locale.interpret Seq.single ((true, Name.name_of name), atts) expr insts)));
    7.32 +            (Locale.interpret Seq.single (true, Name.name_of name) expr insts)));
    7.33  
    7.34  
    7.35  (* classes *)
     8.1 --- a/src/Pure/Isar/locale.ML	Tue Sep 02 16:55:33 2008 +0200
     8.2 +++ b/src/Pure/Isar/locale.ML	Tue Sep 02 17:31:20 2008 +0200
     8.3 @@ -97,21 +97,21 @@
     8.4    val add_declaration: string -> declaration -> Proof.context -> Proof.context
     8.5  
     8.6    val interpretation_i: (Proof.context -> Proof.context) ->
     8.7 -    (bool * string) * Attrib.src list -> expr ->
     8.8 +    bool * string -> expr ->
     8.9      term option list * (Attrib.binding * term) list ->
    8.10      theory -> Proof.state
    8.11    val interpretation: (Proof.context -> Proof.context) ->
    8.12 -    (bool * string) * Attrib.src list -> expr ->
    8.13 +    bool * string -> expr ->
    8.14      string option list * (Attrib.binding * string) list ->
    8.15      theory -> Proof.state
    8.16    val interpretation_in_locale: (Proof.context -> Proof.context) ->
    8.17      xstring * expr -> theory -> Proof.state
    8.18    val interpret_i: (Proof.state -> Proof.state Seq.seq) ->
    8.19 -    (bool * string) * Attrib.src list -> expr ->
    8.20 +    bool * string -> expr ->
    8.21      term option list * (Attrib.binding * term) list ->
    8.22      bool -> Proof.state -> Proof.state
    8.23    val interpret: (Proof.state -> Proof.state Seq.seq) ->
    8.24 -    (bool * string) * Attrib.src list -> expr ->
    8.25 +    bool * string -> expr ->
    8.26      string option list * (Attrib.binding * string) list ->
    8.27      bool -> Proof.state -> Proof.state
    8.28  end;
    8.29 @@ -202,7 +202,7 @@
    8.30  (** management of registrations in theories and proof contexts **)
    8.31  
    8.32  type registration =
    8.33 -  {attn: (bool * string) * Attrib.src list,
    8.34 +  {prfx: bool * string,
    8.35        (* parameters and prefix
    8.36         (if the Boolean flag is set, only accesses containing the prefix are generated,
    8.37          otherwise the prefix may be omitted when accessing theorems etc.) *)
    8.38 @@ -223,20 +223,18 @@
    8.39      val join: T * T -> T
    8.40      val dest: theory -> T ->
    8.41        (term list *
    8.42 -        (((bool * string) * Attrib.src list) *
    8.43 +        ((bool * string) *
    8.44           (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) *
    8.45           Element.witness list *
    8.46           thm Termtab.table)) list
    8.47      val test: theory -> T * term list -> bool
    8.48      val lookup: theory ->
    8.49        T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
    8.50 -      (((bool * string) * Attrib.src list) *
    8.51 -        Element.witness list *
    8.52 -        thm Termtab.table) option
    8.53 -    val insert: theory -> term list -> ((bool * string) * Attrib.src list) ->
    8.54 +      ((bool * string) * Element.witness list * thm Termtab.table) option
    8.55 +    val insert: theory -> term list -> (bool * string) ->
    8.56        (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
    8.57        T ->
    8.58 -      T * (term list * (((bool * string) * Attrib.src list) * Element.witness list)) list
    8.59 +      T * (term list * ((bool * string) * Element.witness list)) list
    8.60      val add_witness: term list -> Element.witness -> T -> T
    8.61      val add_equation: term list -> thm -> T -> T
    8.62    end =
    8.63 @@ -245,14 +243,14 @@
    8.64       NB: index is exported whereas content is internalised. *)
    8.65    type T = registration Termtab.table;
    8.66  
    8.67 -  fun mk_reg attn exp imp wits eqns =
    8.68 -    {attn = attn, exp = exp, imp = imp, wits = wits, eqns = eqns};
    8.69 +  fun mk_reg prfx exp imp wits eqns =
    8.70 +    {prfx = prfx, exp = exp, imp = imp, wits = wits, eqns = eqns};
    8.71  
    8.72    fun map_reg f reg =
    8.73      let
    8.74 -      val {attn, exp, imp, wits, eqns} = reg;
    8.75 -      val (attn', exp', imp', wits', eqns') = f (attn, exp, imp, wits, eqns);
    8.76 -    in mk_reg attn' exp' imp' wits' eqns' end;
    8.77 +      val {prfx, exp, imp, wits, eqns} = reg;
    8.78 +      val (prfx', exp', imp', wits', eqns') = f (prfx, exp, imp, wits, eqns);
    8.79 +    in mk_reg prfx' exp' imp' wits' eqns' end;
    8.80  
    8.81    val empty = Termtab.empty;
    8.82  
    8.83 @@ -265,11 +263,11 @@
    8.84      in ut t [] end;
    8.85  
    8.86    (* joining of registrations:
    8.87 -     - prefix, attributes and morphisms of right theory;
    8.88 +     - prefix and morphisms of right theory;
    8.89       - witnesses are equal, no attempt to subsumption testing;
    8.90       - union of equalities, if conflicting (i.e. two eqns with equal lhs)
    8.91         eqn of right theory takes precedence *)
    8.92 -  fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {attn = n, exp, imp, wits = w, eqns = e2}) =>
    8.93 +  fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {prfx = n, exp, imp, wits = w, eqns = e2}) =>
    8.94        mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2))) (r1, r2);
    8.95  
    8.96    fun dest_transfer thy regs =
    8.97 @@ -277,7 +275,7 @@
    8.98        (n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es))));
    8.99  
   8.100    fun dest thy regs = dest_transfer thy regs |> map (apfst untermify) |>
   8.101 -    map (apsnd (fn {attn, exp, imp, wits, eqns} => (attn, (exp, imp), wits, eqns)));
   8.102 +    map (apsnd (fn {prfx, exp, imp, wits, eqns} => (prfx, (exp, imp), wits, eqns)));
   8.103  
   8.104    (* registrations that subsume t *)
   8.105    fun subsumers thy t regs =
   8.106 @@ -295,7 +293,7 @@
   8.107      in
   8.108        (case subs of
   8.109          [] => NONE
   8.110 -        | ((t', {attn = (prfx, atts), exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns}) :: _) =>
   8.111 +        | ((t', {prfx, exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns}) :: _) =>
   8.112            let
   8.113              val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
   8.114              val tinst' = domT' |> map (fn (T as TFree (x, _)) =>
   8.115 @@ -305,7 +303,7 @@
   8.116                  (x, t |> Morphism.term exp' |> Envir.subst_vars (tinst, inst)
   8.117                        |> var_inst_term (impT, imp))) |> Symtab.make;
   8.118              val inst'_morph = Element.inst_morphism thy (tinst', inst');
   8.119 -          in SOME ((prfx, map (Args.morph_values inst'_morph) atts),
   8.120 +          in SOME (prfx,
   8.121              map (Element.morph_witness inst'_morph) wits,
   8.122              Termtab.map (Morphism.thm inst'_morph) eqns)
   8.123            end)
   8.124 @@ -313,7 +311,7 @@
   8.125  
   8.126    (* add registration if not subsumed by ones already present,
   8.127       additionally returns registrations that are strictly subsumed *)
   8.128 -  fun insert thy ts attn (exp, imp) regs =
   8.129 +  fun insert thy ts prfx (exp, imp) regs =
   8.130      let
   8.131        val t = termify ts;
   8.132        val subs = subsumers thy t regs ;
   8.133 @@ -321,8 +319,8 @@
   8.134          [] => let
   8.135                  val sups =
   8.136                    filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs);
   8.137 -                val sups' = map (apfst untermify) sups |> map (fn (ts, {attn, wits, ...}) => (ts, (attn, wits)))
   8.138 -              in (Termtab.update (t, mk_reg attn exp imp [] Termtab.empty) regs, sups') end
   8.139 +                val sups' = map (apfst untermify) sups |> map (fn (ts, {prfx, wits, ...}) => (ts, (prfx, wits)))
   8.140 +              in (Termtab.update (t, mk_reg prfx exp imp [] Termtab.empty) regs, sups') end
   8.141        | _ => (regs, []))
   8.142      end;
   8.143  
   8.144 @@ -458,24 +456,24 @@
   8.145  
   8.146  (* add registration to theory or context, ignored if subsumed *)
   8.147  
   8.148 -fun put_registration (name, ps) attn morphs (* wits *) ctxt =
   8.149 +fun put_registration (name, ps) prfx morphs (* wits *) ctxt =
   8.150    RegistrationsData.map (fn regs =>
   8.151      let
   8.152        val thy = Context.theory_of ctxt;
   8.153        val reg = the_default Registrations.empty (Symtab.lookup regs name);
   8.154 -      val (reg', sups) = Registrations.insert thy ps attn morphs (* wits *) reg;
   8.155 +      val (reg', sups) = Registrations.insert thy ps prfx morphs (* wits *) reg;
   8.156        val _ = if not (null sups) then warning
   8.157                  ("Subsumed interpretation(s) of locale " ^
   8.158                   quote (extern thy name) ^
   8.159                   "\nwith the following prefix(es):" ^
   8.160 -                  commas_quote (map (fn (_, (((_, s), _), _)) => s) sups))
   8.161 +                  commas_quote (map (fn (_, ((_, s), _)) => s) sups))
   8.162                else ();
   8.163      in Symtab.update (name, reg') regs end) ctxt;
   8.164  
   8.165 -fun put_global_registration id attn morphs =
   8.166 -  Context.theory_map (put_registration id attn morphs);
   8.167 -fun put_local_registration id attn morphs =
   8.168 -  Context.proof_map (put_registration id attn morphs);
   8.169 +fun put_global_registration id prfx morphs =
   8.170 +  Context.theory_map (put_registration id prfx morphs);
   8.171 +fun put_local_registration id prfx morphs =
   8.172 +  Context.proof_map (put_registration id prfx morphs);
   8.173  
   8.174  
   8.175  fun put_registration_in_locale name id =
   8.176 @@ -522,11 +520,8 @@
   8.177      val prt_thm = prt_term o prop_of;
   8.178      fun prt_inst ts =
   8.179          Pretty.enclose "(" ")" (Pretty.breaks (map prt_term' ts));
   8.180 -    fun prt_attn ((false, prfx), atts) =
   8.181 -        Pretty.breaks (Pretty.str prfx :: Pretty.str "(optional)" ::
   8.182 -          Attrib.pretty_attribs ctxt atts)
   8.183 -      | prt_attn ((true, prfx), atts) =
   8.184 -        Pretty.breaks (Pretty.str prfx :: Attrib.pretty_attribs ctxt atts);
   8.185 +    fun prt_prfx (false, prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str "(optional)"]
   8.186 +      | prt_prfx (true, prfx) = [Pretty.str prfx];
   8.187      fun prt_eqns [] = Pretty.str "no equations."
   8.188        | prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 ::
   8.189            Pretty.breaks (map prt_thm eqns));
   8.190 @@ -535,15 +530,15 @@
   8.191      fun prt_witns [] = Pretty.str "no witnesses."
   8.192        | prt_witns witns = Pretty.block (Pretty.str "witnesses:" :: Pretty.brk 1 ::
   8.193            Pretty.breaks (map (Element.pretty_witness ctxt) witns))
   8.194 -    fun prt_reg (ts, (((_, ""), []), _, witns, eqns)) =
   8.195 +    fun prt_reg (ts, ((_, ""), _, witns, eqns)) =
   8.196          if show_wits
   8.197            then Pretty.block (prt_core ts eqns @ [Pretty.fbrk, prt_witns witns])
   8.198            else Pretty.block (prt_core ts eqns)
   8.199 -      | prt_reg (ts, (attn, _, witns, eqns)) =
   8.200 +      | prt_reg (ts, (prfx, _, witns, eqns)) =
   8.201          if show_wits
   8.202 -          then Pretty.block ((prt_attn attn @ [Pretty.str ":", Pretty.brk 1] @
   8.203 +          then Pretty.block ((prt_prfx prfx @ [Pretty.str ":", Pretty.brk 1] @
   8.204              prt_core ts eqns @ [Pretty.fbrk, prt_witns witns]))
   8.205 -          else Pretty.block ((prt_attn attn @
   8.206 +          else Pretty.block ((prt_prfx prfx @
   8.207              [Pretty.str ":", Pretty.brk 1] @ prt_core ts eqns));
   8.208  
   8.209      val loc_int = intern thy loc;
   8.210 @@ -554,7 +549,7 @@
   8.211          NONE => Pretty.str ("no interpretations")
   8.212        | SOME r => let
   8.213              val r' = Registrations.dest thy r;
   8.214 -            val r'' = Library.sort_wrt (fn (_, (((_, prfx), _), _, _, _)) => prfx) r';
   8.215 +            val r'' = Library.sort_wrt (fn (_, ((_, prfx), _, _, _)) => prfx) r';
   8.216            in Pretty.big_list ("interpretations:") (map prt_reg r'') end)
   8.217      |> Pretty.writeln
   8.218    end;
   8.219 @@ -996,7 +991,7 @@
   8.220                val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
   8.221              in if test_local_registration ctxt' (name, ps') then ctxt'
   8.222                else let
   8.223 -                  val ctxt'' = put_local_registration (name, ps') ((true, ""), [])
   8.224 +                  val ctxt'' = put_local_registration (name, ps') (true, "")
   8.225                      (Morphism.identity, ((Vartab.empty, []), (Vartab.empty, []) )) ctxt'
   8.226                  in case mode of
   8.227                      Assumed axs =>
   8.228 @@ -1652,7 +1647,7 @@
   8.229  
   8.230  (* compute morphism and apply to args *)
   8.231  
   8.232 -fun interpret_args thy prfx insts prems eqns atts2 exp attrib args =
   8.233 +fun interpret_args thy prfx insts prems eqns exp attrib args =
   8.234    let
   8.235      val inst = Morphism.name_morphism (Name.map_name (NameSpace.qualified prfx)) $>
   8.236  (* need to add parameter prefix *) (* FIXME *)
   8.237 @@ -1662,8 +1657,6 @@
   8.238    in
   8.239      args |> Element.facts_map (morph_ctxt' inst) |>
   8.240  (* suppresses application of name morphism: workaroud for class package *) (* FIXME *)
   8.241 -      map (fn (attn, bs) => (attn,
   8.242 -        bs |> map (fn (ths, atts) => (ths, (atts @ atts2))))) |>
   8.243        standardize thy exp |> Attrib.map_facts attrib
   8.244    end;
   8.245  
   8.246 @@ -1680,12 +1673,12 @@
   8.247      val regs = get_global_registrations thy target;
   8.248      (* add args to thy for all registrations *)
   8.249  
   8.250 -    fun activate (vts, (((fully_qualified, prfx), atts2), (exp, imp), _, _)) thy =
   8.251 +    fun activate (vts, ((fully_qualified, prfx), (exp, imp), _, _)) thy =
   8.252        let
   8.253          val (insts, prems, eqns) = collect_global_witnesses thy imp parms ids vts;
   8.254          val attrib = Attrib.attribute_i thy;
   8.255          val args' = args
   8.256 -          |> interpret_args thy prfx insts prems eqns atts2 exp attrib
   8.257 +          |> interpret_args thy prfx insts prems eqns exp attrib
   8.258            |> add_param_prefixss (space_implode "_" (map fst parms));
   8.259        in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end;
   8.260    in fold activate regs thy end;
   8.261 @@ -2059,7 +2052,7 @@
   8.262      val ord = prod_ord string_ord (list_ord Term.fast_term_ord));
   8.263  
   8.264  fun gen_activate_facts_elemss mk_ctxt get_reg note note_interp attrib put_reg test_reg add_wit add_eqn
   8.265 -        attn all_elemss propss eq_attns (exp, imp) thmss thy_ctxt =
   8.266 +        prfx all_elemss propss eq_attns (exp, imp) thmss thy_ctxt =
   8.267    let
   8.268      val ctxt = mk_ctxt thy_ctxt;
   8.269      val (all_propss, eq_props) = chop (length all_elemss) propss;
   8.270 @@ -2073,8 +2066,8 @@
   8.271  
   8.272      val thy_ctxt' = thy_ctxt
   8.273        (* add registrations *)
   8.274 -(*      |> fold (fn ((id, _), _) => put_reg id attn (exp, imp)) new_elemss *)
   8.275 -      |> fold (fn (id, _) => put_reg id attn (exp, imp)) new_propss
   8.276 +(*      |> fold (fn ((id, _), _) => put_reg id prfx (exp, imp)) new_elemss *)
   8.277 +      |> fold (fn (id, _) => put_reg id prfx (exp, imp)) new_propss
   8.278        (* add witnesses of Assumed elements (only those generate proof obligations) *)
   8.279        |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst new_propss ~~ new_thmss)
   8.280        (* add equations *)
   8.281 @@ -2086,22 +2079,21 @@
   8.282            (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id)
   8.283              | ((_, Derived _), _) => NONE) all_elemss);
   8.284  
   8.285 -    fun activate_elem eqns loc ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt =
   8.286 +    fun activate_elem eqns loc (fully_qualified, prfx) (Notes (kind, facts)) thy_ctxt =
   8.287          let
   8.288            val ctxt = mk_ctxt thy_ctxt;
   8.289            val facts' = interpret_args (ProofContext.theory_of ctxt) prfx
   8.290 -              (Symtab.empty, Symtab.empty) prems eqns atts
   8.291 -              exp (attrib thy_ctxt) facts;
   8.292 +              (Symtab.empty, Symtab.empty) prems eqns exp (attrib thy_ctxt) facts;
   8.293          in snd (note_interp kind loc (fully_qualified, prfx) facts' thy_ctxt) end
   8.294        | activate_elem _ _ _ _ thy_ctxt = thy_ctxt;
   8.295  
   8.296      fun activate_elems all_eqns ((id, _), elems) thy_ctxt =
   8.297        let
   8.298 -        val (prfx_atts, _, _) = case get_reg thy_ctxt imp id
   8.299 +        val (prfx, _, _) = case get_reg thy_ctxt imp id
   8.300           of SOME x => x
   8.301            | NONE => sys_error ("Unknown registration of " ^ quote (fst id)
   8.302                ^ " while activating facts.");
   8.303 -      in fold (activate_elem (the (Idtab.lookup all_eqns id)) (fst id) prfx_atts) elems thy_ctxt end;
   8.304 +      in fold (activate_elem (the (Idtab.lookup all_eqns id)) (fst id) prfx) elems thy_ctxt end;
   8.305  
   8.306      val thy_ctxt'' = thy_ctxt'
   8.307        (* add witnesses of Derived elements *)
   8.308 @@ -2209,7 +2201,7 @@
   8.309  
   8.310  fun gen_prep_registration mk_ctxt test_reg activate
   8.311      prep_attr prep_expr prep_insts
   8.312 -    thy_ctxt raw_attn raw_expr raw_insts =
   8.313 +    thy_ctxt prfx raw_expr raw_insts =
   8.314    let
   8.315      val ctxt = mk_ctxt thy_ctxt;
   8.316      val thy = ProofContext.theory_of ctxt;
   8.317 @@ -2217,7 +2209,6 @@
   8.318      fun prep_attn attn = (apsnd o map)
   8.319        (Attrib.crude_closure ctxt o Args.assignable o prep_attr thy) attn;
   8.320  
   8.321 -    val attn = prep_attn raw_attn;
   8.322      val expr = prep_expr thy raw_expr;
   8.323  
   8.324      val pts = params_of_expr ctxt' [] expr ([], Symtab.empty, Symtab.empty);
   8.325 @@ -2274,7 +2265,7 @@
   8.326  
   8.327      val propss = map extract_asms_elems inst_elemss @ eqn_elems;
   8.328  
   8.329 -  in (propss, activate attn inst_elemss propss eq_attns morphs) end;
   8.330 +  in (propss, activate prfx inst_elemss propss eq_attns morphs) end;
   8.331  
   8.332  fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init
   8.333    test_global_registration
   8.334 @@ -2333,7 +2324,7 @@
   8.335                  |> fold (add_witness_in_locale target id) thms
   8.336            | activate_id _ thy = thy;
   8.337  
   8.338 -        fun activate_reg (vts, (((fully_qualified, prfx), atts2), (exp, imp), _, _)) thy =
   8.339 +        fun activate_reg (vts, ((fully_qualified, prfx), (exp, imp), _, _)) thy =
   8.340            let
   8.341              val (insts, wits, _) = collect_global_witnesses thy imp fixed target_ids vts;
   8.342              fun inst_parms ps = map
   8.343 @@ -2348,7 +2339,7 @@
   8.344                  if test_global_registration thy (name, ps')
   8.345                  then thy
   8.346                  else thy
   8.347 -                  |> put_global_registration (name, ps') ((fully_qualified, prfx), atts2) (exp, imp)
   8.348 +                  |> put_global_registration (name, ps') (fully_qualified, prfx) (exp, imp)
   8.349                    |> fold (fn witn => fn thy => add_global_witness (name, ps')
   8.350                       (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms
   8.351                end;
   8.352 @@ -2360,7 +2351,7 @@
   8.353                  if test_global_registration thy (name, ps')
   8.354                  then thy
   8.355                  else thy
   8.356 -                  |> put_global_registration (name, ps') ((fully_qualified, prfx), atts2) (exp, imp)
   8.357 +                  |> put_global_registration (name, ps') (fully_qualified, prfx) (exp, imp)
   8.358                    |> fold (fn witn => fn thy => add_global_witness (name, ps')
   8.359                         (witn |> Element.map_witness (fn (t, th) =>  (* FIXME *)
   8.360                         (Element.inst_term insts t,
   8.361 @@ -2376,7 +2367,6 @@
   8.362                      Morphism.thm_morphism disch;
   8.363                    val facts' = facts
   8.364                      |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism)
   8.365 -                    |> map (apfst (apsnd (fn a => a @ map (Attrib.attribute thy) atts2)))
   8.366                      |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
   8.367                  in
   8.368                    thy
   8.369 @@ -2403,10 +2393,10 @@
   8.370  fun prep_result propps thmss =
   8.371    ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss);
   8.372  
   8.373 -fun gen_interpretation prep_registration after_qed (prfx, raw_atts) raw_expr raw_insts thy =
   8.374 +fun gen_interpretation prep_registration after_qed prfx raw_expr raw_insts thy =
   8.375    (* prfx = (flag indicating full qualification, name prefix) *)
   8.376    let
   8.377 -    val (propss, activate) = prep_registration thy (prfx, raw_atts) raw_expr raw_insts;
   8.378 +    val (propss, activate) = prep_registration thy prfx raw_expr raw_insts;
   8.379      fun after_qed' results =
   8.380        ProofContext.theory (activate (prep_result propss results))
   8.381        #> after_qed;
   8.382 @@ -2418,12 +2408,12 @@
   8.383      |> Seq.hd
   8.384    end;
   8.385  
   8.386 -fun gen_interpret prep_registration after_qed (prfx, atts) expr insts int state =
   8.387 +fun gen_interpret prep_registration after_qed prfx expr insts int state =
   8.388    (* prfx = (flag indicating full qualification, name prefix) *)
   8.389    let
   8.390      val _ = Proof.assert_forward_or_chain state;
   8.391      val ctxt = Proof.context_of state;
   8.392 -    val (propss, activate) = prep_registration ctxt (prfx, atts) expr insts;
   8.393 +    val (propss, activate) = prep_registration ctxt prfx expr insts;
   8.394      fun after_qed' results =
   8.395        Proof.map_context (K (ctxt |> activate (prep_result propss results)))
   8.396        #> Proof.put_facts NONE