src/Pure/Isar/locale.ML
changeset 28085 914183e229e9
parent 28084 a05ca48ef263
child 28107 760ecc6fc1bd
     1.1 --- a/src/Pure/Isar/locale.ML	Tue Sep 02 16:55:33 2008 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Tue Sep 02 17:31:20 2008 +0200
     1.3 @@ -97,21 +97,21 @@
     1.4    val add_declaration: string -> declaration -> Proof.context -> Proof.context
     1.5  
     1.6    val interpretation_i: (Proof.context -> Proof.context) ->
     1.7 -    (bool * string) * Attrib.src list -> expr ->
     1.8 +    bool * string -> expr ->
     1.9      term option list * (Attrib.binding * term) list ->
    1.10      theory -> Proof.state
    1.11    val interpretation: (Proof.context -> Proof.context) ->
    1.12 -    (bool * string) * Attrib.src list -> expr ->
    1.13 +    bool * string -> expr ->
    1.14      string option list * (Attrib.binding * string) list ->
    1.15      theory -> Proof.state
    1.16    val interpretation_in_locale: (Proof.context -> Proof.context) ->
    1.17      xstring * expr -> theory -> Proof.state
    1.18    val interpret_i: (Proof.state -> Proof.state Seq.seq) ->
    1.19 -    (bool * string) * Attrib.src list -> expr ->
    1.20 +    bool * string -> expr ->
    1.21      term option list * (Attrib.binding * term) list ->
    1.22      bool -> Proof.state -> Proof.state
    1.23    val interpret: (Proof.state -> Proof.state Seq.seq) ->
    1.24 -    (bool * string) * Attrib.src list -> expr ->
    1.25 +    bool * string -> expr ->
    1.26      string option list * (Attrib.binding * string) list ->
    1.27      bool -> Proof.state -> Proof.state
    1.28  end;
    1.29 @@ -202,7 +202,7 @@
    1.30  (** management of registrations in theories and proof contexts **)
    1.31  
    1.32  type registration =
    1.33 -  {attn: (bool * string) * Attrib.src list,
    1.34 +  {prfx: bool * string,
    1.35        (* parameters and prefix
    1.36         (if the Boolean flag is set, only accesses containing the prefix are generated,
    1.37          otherwise the prefix may be omitted when accessing theorems etc.) *)
    1.38 @@ -223,20 +223,18 @@
    1.39      val join: T * T -> T
    1.40      val dest: theory -> T ->
    1.41        (term list *
    1.42 -        (((bool * string) * Attrib.src list) *
    1.43 +        ((bool * string) *
    1.44           (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) *
    1.45           Element.witness list *
    1.46           thm Termtab.table)) list
    1.47      val test: theory -> T * term list -> bool
    1.48      val lookup: theory ->
    1.49        T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
    1.50 -      (((bool * string) * Attrib.src list) *
    1.51 -        Element.witness list *
    1.52 -        thm Termtab.table) option
    1.53 -    val insert: theory -> term list -> ((bool * string) * Attrib.src list) ->
    1.54 +      ((bool * string) * Element.witness list * thm Termtab.table) option
    1.55 +    val insert: theory -> term list -> (bool * string) ->
    1.56        (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
    1.57        T ->
    1.58 -      T * (term list * (((bool * string) * Attrib.src list) * Element.witness list)) list
    1.59 +      T * (term list * ((bool * string) * Element.witness list)) list
    1.60      val add_witness: term list -> Element.witness -> T -> T
    1.61      val add_equation: term list -> thm -> T -> T
    1.62    end =
    1.63 @@ -245,14 +243,14 @@
    1.64       NB: index is exported whereas content is internalised. *)
    1.65    type T = registration Termtab.table;
    1.66  
    1.67 -  fun mk_reg attn exp imp wits eqns =
    1.68 -    {attn = attn, exp = exp, imp = imp, wits = wits, eqns = eqns};
    1.69 +  fun mk_reg prfx exp imp wits eqns =
    1.70 +    {prfx = prfx, exp = exp, imp = imp, wits = wits, eqns = eqns};
    1.71  
    1.72    fun map_reg f reg =
    1.73      let
    1.74 -      val {attn, exp, imp, wits, eqns} = reg;
    1.75 -      val (attn', exp', imp', wits', eqns') = f (attn, exp, imp, wits, eqns);
    1.76 -    in mk_reg attn' exp' imp' wits' eqns' end;
    1.77 +      val {prfx, exp, imp, wits, eqns} = reg;
    1.78 +      val (prfx', exp', imp', wits', eqns') = f (prfx, exp, imp, wits, eqns);
    1.79 +    in mk_reg prfx' exp' imp' wits' eqns' end;
    1.80  
    1.81    val empty = Termtab.empty;
    1.82  
    1.83 @@ -265,11 +263,11 @@
    1.84      in ut t [] end;
    1.85  
    1.86    (* joining of registrations:
    1.87 -     - prefix, attributes and morphisms of right theory;
    1.88 +     - prefix and morphisms of right theory;
    1.89       - witnesses are equal, no attempt to subsumption testing;
    1.90       - union of equalities, if conflicting (i.e. two eqns with equal lhs)
    1.91         eqn of right theory takes precedence *)
    1.92 -  fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {attn = n, exp, imp, wits = w, eqns = e2}) =>
    1.93 +  fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {prfx = n, exp, imp, wits = w, eqns = e2}) =>
    1.94        mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2))) (r1, r2);
    1.95  
    1.96    fun dest_transfer thy regs =
    1.97 @@ -277,7 +275,7 @@
    1.98        (n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es))));
    1.99  
   1.100    fun dest thy regs = dest_transfer thy regs |> map (apfst untermify) |>
   1.101 -    map (apsnd (fn {attn, exp, imp, wits, eqns} => (attn, (exp, imp), wits, eqns)));
   1.102 +    map (apsnd (fn {prfx, exp, imp, wits, eqns} => (prfx, (exp, imp), wits, eqns)));
   1.103  
   1.104    (* registrations that subsume t *)
   1.105    fun subsumers thy t regs =
   1.106 @@ -295,7 +293,7 @@
   1.107      in
   1.108        (case subs of
   1.109          [] => NONE
   1.110 -        | ((t', {attn = (prfx, atts), exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns}) :: _) =>
   1.111 +        | ((t', {prfx, exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns}) :: _) =>
   1.112            let
   1.113              val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
   1.114              val tinst' = domT' |> map (fn (T as TFree (x, _)) =>
   1.115 @@ -305,7 +303,7 @@
   1.116                  (x, t |> Morphism.term exp' |> Envir.subst_vars (tinst, inst)
   1.117                        |> var_inst_term (impT, imp))) |> Symtab.make;
   1.118              val inst'_morph = Element.inst_morphism thy (tinst', inst');
   1.119 -          in SOME ((prfx, map (Args.morph_values inst'_morph) atts),
   1.120 +          in SOME (prfx,
   1.121              map (Element.morph_witness inst'_morph) wits,
   1.122              Termtab.map (Morphism.thm inst'_morph) eqns)
   1.123            end)
   1.124 @@ -313,7 +311,7 @@
   1.125  
   1.126    (* add registration if not subsumed by ones already present,
   1.127       additionally returns registrations that are strictly subsumed *)
   1.128 -  fun insert thy ts attn (exp, imp) regs =
   1.129 +  fun insert thy ts prfx (exp, imp) regs =
   1.130      let
   1.131        val t = termify ts;
   1.132        val subs = subsumers thy t regs ;
   1.133 @@ -321,8 +319,8 @@
   1.134          [] => let
   1.135                  val sups =
   1.136                    filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs);
   1.137 -                val sups' = map (apfst untermify) sups |> map (fn (ts, {attn, wits, ...}) => (ts, (attn, wits)))
   1.138 -              in (Termtab.update (t, mk_reg attn exp imp [] Termtab.empty) regs, sups') end
   1.139 +                val sups' = map (apfst untermify) sups |> map (fn (ts, {prfx, wits, ...}) => (ts, (prfx, wits)))
   1.140 +              in (Termtab.update (t, mk_reg prfx exp imp [] Termtab.empty) regs, sups') end
   1.141        | _ => (regs, []))
   1.142      end;
   1.143  
   1.144 @@ -458,24 +456,24 @@
   1.145  
   1.146  (* add registration to theory or context, ignored if subsumed *)
   1.147  
   1.148 -fun put_registration (name, ps) attn morphs (* wits *) ctxt =
   1.149 +fun put_registration (name, ps) prfx morphs (* wits *) ctxt =
   1.150    RegistrationsData.map (fn regs =>
   1.151      let
   1.152        val thy = Context.theory_of ctxt;
   1.153        val reg = the_default Registrations.empty (Symtab.lookup regs name);
   1.154 -      val (reg', sups) = Registrations.insert thy ps attn morphs (* wits *) reg;
   1.155 +      val (reg', sups) = Registrations.insert thy ps prfx morphs (* wits *) reg;
   1.156        val _ = if not (null sups) then warning
   1.157                  ("Subsumed interpretation(s) of locale " ^
   1.158                   quote (extern thy name) ^
   1.159                   "\nwith the following prefix(es):" ^
   1.160 -                  commas_quote (map (fn (_, (((_, s), _), _)) => s) sups))
   1.161 +                  commas_quote (map (fn (_, ((_, s), _)) => s) sups))
   1.162                else ();
   1.163      in Symtab.update (name, reg') regs end) ctxt;
   1.164  
   1.165 -fun put_global_registration id attn morphs =
   1.166 -  Context.theory_map (put_registration id attn morphs);
   1.167 -fun put_local_registration id attn morphs =
   1.168 -  Context.proof_map (put_registration id attn morphs);
   1.169 +fun put_global_registration id prfx morphs =
   1.170 +  Context.theory_map (put_registration id prfx morphs);
   1.171 +fun put_local_registration id prfx morphs =
   1.172 +  Context.proof_map (put_registration id prfx morphs);
   1.173  
   1.174  
   1.175  fun put_registration_in_locale name id =
   1.176 @@ -522,11 +520,8 @@
   1.177      val prt_thm = prt_term o prop_of;
   1.178      fun prt_inst ts =
   1.179          Pretty.enclose "(" ")" (Pretty.breaks (map prt_term' ts));
   1.180 -    fun prt_attn ((false, prfx), atts) =
   1.181 -        Pretty.breaks (Pretty.str prfx :: Pretty.str "(optional)" ::
   1.182 -          Attrib.pretty_attribs ctxt atts)
   1.183 -      | prt_attn ((true, prfx), atts) =
   1.184 -        Pretty.breaks (Pretty.str prfx :: Attrib.pretty_attribs ctxt atts);
   1.185 +    fun prt_prfx (false, prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str "(optional)"]
   1.186 +      | prt_prfx (true, prfx) = [Pretty.str prfx];
   1.187      fun prt_eqns [] = Pretty.str "no equations."
   1.188        | prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 ::
   1.189            Pretty.breaks (map prt_thm eqns));
   1.190 @@ -535,15 +530,15 @@
   1.191      fun prt_witns [] = Pretty.str "no witnesses."
   1.192        | prt_witns witns = Pretty.block (Pretty.str "witnesses:" :: Pretty.brk 1 ::
   1.193            Pretty.breaks (map (Element.pretty_witness ctxt) witns))
   1.194 -    fun prt_reg (ts, (((_, ""), []), _, witns, eqns)) =
   1.195 +    fun prt_reg (ts, ((_, ""), _, witns, eqns)) =
   1.196          if show_wits
   1.197            then Pretty.block (prt_core ts eqns @ [Pretty.fbrk, prt_witns witns])
   1.198            else Pretty.block (prt_core ts eqns)
   1.199 -      | prt_reg (ts, (attn, _, witns, eqns)) =
   1.200 +      | prt_reg (ts, (prfx, _, witns, eqns)) =
   1.201          if show_wits
   1.202 -          then Pretty.block ((prt_attn attn @ [Pretty.str ":", Pretty.brk 1] @
   1.203 +          then Pretty.block ((prt_prfx prfx @ [Pretty.str ":", Pretty.brk 1] @
   1.204              prt_core ts eqns @ [Pretty.fbrk, prt_witns witns]))
   1.205 -          else Pretty.block ((prt_attn attn @
   1.206 +          else Pretty.block ((prt_prfx prfx @
   1.207              [Pretty.str ":", Pretty.brk 1] @ prt_core ts eqns));
   1.208  
   1.209      val loc_int = intern thy loc;
   1.210 @@ -554,7 +549,7 @@
   1.211          NONE => Pretty.str ("no interpretations")
   1.212        | SOME r => let
   1.213              val r' = Registrations.dest thy r;
   1.214 -            val r'' = Library.sort_wrt (fn (_, (((_, prfx), _), _, _, _)) => prfx) r';
   1.215 +            val r'' = Library.sort_wrt (fn (_, ((_, prfx), _, _, _)) => prfx) r';
   1.216            in Pretty.big_list ("interpretations:") (map prt_reg r'') end)
   1.217      |> Pretty.writeln
   1.218    end;
   1.219 @@ -996,7 +991,7 @@
   1.220                val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
   1.221              in if test_local_registration ctxt' (name, ps') then ctxt'
   1.222                else let
   1.223 -                  val ctxt'' = put_local_registration (name, ps') ((true, ""), [])
   1.224 +                  val ctxt'' = put_local_registration (name, ps') (true, "")
   1.225                      (Morphism.identity, ((Vartab.empty, []), (Vartab.empty, []) )) ctxt'
   1.226                  in case mode of
   1.227                      Assumed axs =>
   1.228 @@ -1652,7 +1647,7 @@
   1.229  
   1.230  (* compute morphism and apply to args *)
   1.231  
   1.232 -fun interpret_args thy prfx insts prems eqns atts2 exp attrib args =
   1.233 +fun interpret_args thy prfx insts prems eqns exp attrib args =
   1.234    let
   1.235      val inst = Morphism.name_morphism (Name.map_name (NameSpace.qualified prfx)) $>
   1.236  (* need to add parameter prefix *) (* FIXME *)
   1.237 @@ -1662,8 +1657,6 @@
   1.238    in
   1.239      args |> Element.facts_map (morph_ctxt' inst) |>
   1.240  (* suppresses application of name morphism: workaroud for class package *) (* FIXME *)
   1.241 -      map (fn (attn, bs) => (attn,
   1.242 -        bs |> map (fn (ths, atts) => (ths, (atts @ atts2))))) |>
   1.243        standardize thy exp |> Attrib.map_facts attrib
   1.244    end;
   1.245  
   1.246 @@ -1680,12 +1673,12 @@
   1.247      val regs = get_global_registrations thy target;
   1.248      (* add args to thy for all registrations *)
   1.249  
   1.250 -    fun activate (vts, (((fully_qualified, prfx), atts2), (exp, imp), _, _)) thy =
   1.251 +    fun activate (vts, ((fully_qualified, prfx), (exp, imp), _, _)) thy =
   1.252        let
   1.253          val (insts, prems, eqns) = collect_global_witnesses thy imp parms ids vts;
   1.254          val attrib = Attrib.attribute_i thy;
   1.255          val args' = args
   1.256 -          |> interpret_args thy prfx insts prems eqns atts2 exp attrib
   1.257 +          |> interpret_args thy prfx insts prems eqns exp attrib
   1.258            |> add_param_prefixss (space_implode "_" (map fst parms));
   1.259        in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end;
   1.260    in fold activate regs thy end;
   1.261 @@ -2059,7 +2052,7 @@
   1.262      val ord = prod_ord string_ord (list_ord Term.fast_term_ord));
   1.263  
   1.264  fun gen_activate_facts_elemss mk_ctxt get_reg note note_interp attrib put_reg test_reg add_wit add_eqn
   1.265 -        attn all_elemss propss eq_attns (exp, imp) thmss thy_ctxt =
   1.266 +        prfx all_elemss propss eq_attns (exp, imp) thmss thy_ctxt =
   1.267    let
   1.268      val ctxt = mk_ctxt thy_ctxt;
   1.269      val (all_propss, eq_props) = chop (length all_elemss) propss;
   1.270 @@ -2073,8 +2066,8 @@
   1.271  
   1.272      val thy_ctxt' = thy_ctxt
   1.273        (* add registrations *)
   1.274 -(*      |> fold (fn ((id, _), _) => put_reg id attn (exp, imp)) new_elemss *)
   1.275 -      |> fold (fn (id, _) => put_reg id attn (exp, imp)) new_propss
   1.276 +(*      |> fold (fn ((id, _), _) => put_reg id prfx (exp, imp)) new_elemss *)
   1.277 +      |> fold (fn (id, _) => put_reg id prfx (exp, imp)) new_propss
   1.278        (* add witnesses of Assumed elements (only those generate proof obligations) *)
   1.279        |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst new_propss ~~ new_thmss)
   1.280        (* add equations *)
   1.281 @@ -2086,22 +2079,21 @@
   1.282            (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id)
   1.283              | ((_, Derived _), _) => NONE) all_elemss);
   1.284  
   1.285 -    fun activate_elem eqns loc ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt =
   1.286 +    fun activate_elem eqns loc (fully_qualified, prfx) (Notes (kind, facts)) thy_ctxt =
   1.287          let
   1.288            val ctxt = mk_ctxt thy_ctxt;
   1.289            val facts' = interpret_args (ProofContext.theory_of ctxt) prfx
   1.290 -              (Symtab.empty, Symtab.empty) prems eqns atts
   1.291 -              exp (attrib thy_ctxt) facts;
   1.292 +              (Symtab.empty, Symtab.empty) prems eqns exp (attrib thy_ctxt) facts;
   1.293          in snd (note_interp kind loc (fully_qualified, prfx) facts' thy_ctxt) end
   1.294        | activate_elem _ _ _ _ thy_ctxt = thy_ctxt;
   1.295  
   1.296      fun activate_elems all_eqns ((id, _), elems) thy_ctxt =
   1.297        let
   1.298 -        val (prfx_atts, _, _) = case get_reg thy_ctxt imp id
   1.299 +        val (prfx, _, _) = case get_reg thy_ctxt imp id
   1.300           of SOME x => x
   1.301            | NONE => sys_error ("Unknown registration of " ^ quote (fst id)
   1.302                ^ " while activating facts.");
   1.303 -      in fold (activate_elem (the (Idtab.lookup all_eqns id)) (fst id) prfx_atts) elems thy_ctxt end;
   1.304 +      in fold (activate_elem (the (Idtab.lookup all_eqns id)) (fst id) prfx) elems thy_ctxt end;
   1.305  
   1.306      val thy_ctxt'' = thy_ctxt'
   1.307        (* add witnesses of Derived elements *)
   1.308 @@ -2209,7 +2201,7 @@
   1.309  
   1.310  fun gen_prep_registration mk_ctxt test_reg activate
   1.311      prep_attr prep_expr prep_insts
   1.312 -    thy_ctxt raw_attn raw_expr raw_insts =
   1.313 +    thy_ctxt prfx raw_expr raw_insts =
   1.314    let
   1.315      val ctxt = mk_ctxt thy_ctxt;
   1.316      val thy = ProofContext.theory_of ctxt;
   1.317 @@ -2217,7 +2209,6 @@
   1.318      fun prep_attn attn = (apsnd o map)
   1.319        (Attrib.crude_closure ctxt o Args.assignable o prep_attr thy) attn;
   1.320  
   1.321 -    val attn = prep_attn raw_attn;
   1.322      val expr = prep_expr thy raw_expr;
   1.323  
   1.324      val pts = params_of_expr ctxt' [] expr ([], Symtab.empty, Symtab.empty);
   1.325 @@ -2274,7 +2265,7 @@
   1.326  
   1.327      val propss = map extract_asms_elems inst_elemss @ eqn_elems;
   1.328  
   1.329 -  in (propss, activate attn inst_elemss propss eq_attns morphs) end;
   1.330 +  in (propss, activate prfx inst_elemss propss eq_attns morphs) end;
   1.331  
   1.332  fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init
   1.333    test_global_registration
   1.334 @@ -2333,7 +2324,7 @@
   1.335                  |> fold (add_witness_in_locale target id) thms
   1.336            | activate_id _ thy = thy;
   1.337  
   1.338 -        fun activate_reg (vts, (((fully_qualified, prfx), atts2), (exp, imp), _, _)) thy =
   1.339 +        fun activate_reg (vts, ((fully_qualified, prfx), (exp, imp), _, _)) thy =
   1.340            let
   1.341              val (insts, wits, _) = collect_global_witnesses thy imp fixed target_ids vts;
   1.342              fun inst_parms ps = map
   1.343 @@ -2348,7 +2339,7 @@
   1.344                  if test_global_registration thy (name, ps')
   1.345                  then thy
   1.346                  else thy
   1.347 -                  |> put_global_registration (name, ps') ((fully_qualified, prfx), atts2) (exp, imp)
   1.348 +                  |> put_global_registration (name, ps') (fully_qualified, prfx) (exp, imp)
   1.349                    |> fold (fn witn => fn thy => add_global_witness (name, ps')
   1.350                       (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms
   1.351                end;
   1.352 @@ -2360,7 +2351,7 @@
   1.353                  if test_global_registration thy (name, ps')
   1.354                  then thy
   1.355                  else thy
   1.356 -                  |> put_global_registration (name, ps') ((fully_qualified, prfx), atts2) (exp, imp)
   1.357 +                  |> put_global_registration (name, ps') (fully_qualified, prfx) (exp, imp)
   1.358                    |> fold (fn witn => fn thy => add_global_witness (name, ps')
   1.359                         (witn |> Element.map_witness (fn (t, th) =>  (* FIXME *)
   1.360                         (Element.inst_term insts t,
   1.361 @@ -2376,7 +2367,6 @@
   1.362                      Morphism.thm_morphism disch;
   1.363                    val facts' = facts
   1.364                      |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism)
   1.365 -                    |> map (apfst (apsnd (fn a => a @ map (Attrib.attribute thy) atts2)))
   1.366                      |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
   1.367                  in
   1.368                    thy
   1.369 @@ -2403,10 +2393,10 @@
   1.370  fun prep_result propps thmss =
   1.371    ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss);
   1.372  
   1.373 -fun gen_interpretation prep_registration after_qed (prfx, raw_atts) raw_expr raw_insts thy =
   1.374 +fun gen_interpretation prep_registration after_qed prfx raw_expr raw_insts thy =
   1.375    (* prfx = (flag indicating full qualification, name prefix) *)
   1.376    let
   1.377 -    val (propss, activate) = prep_registration thy (prfx, raw_atts) raw_expr raw_insts;
   1.378 +    val (propss, activate) = prep_registration thy prfx raw_expr raw_insts;
   1.379      fun after_qed' results =
   1.380        ProofContext.theory (activate (prep_result propss results))
   1.381        #> after_qed;
   1.382 @@ -2418,12 +2408,12 @@
   1.383      |> Seq.hd
   1.384    end;
   1.385  
   1.386 -fun gen_interpret prep_registration after_qed (prfx, atts) expr insts int state =
   1.387 +fun gen_interpret prep_registration after_qed prfx expr insts int state =
   1.388    (* prfx = (flag indicating full qualification, name prefix) *)
   1.389    let
   1.390      val _ = Proof.assert_forward_or_chain state;
   1.391      val ctxt = Proof.context_of state;
   1.392 -    val (propss, activate) = prep_registration ctxt (prfx, atts) expr insts;
   1.393 +    val (propss, activate) = prep_registration ctxt prfx expr insts;
   1.394      fun after_qed' results =
   1.395        Proof.map_context (K (ctxt |> activate (prep_result propss results)))
   1.396        #> Proof.put_facts NONE