explicit name morphism function for locale interpretation
authorhaftmann
Mon Nov 17 17:00:27 2008 +0100 (2008-11-17)
changeset 288227ca11ecbc4fb
parent 28821 78a6ed46ad04
child 28823 dcbef866c9e2
explicit name morphism function for locale interpretation
src/Pure/Isar/class.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/class.ML	Mon Nov 17 17:00:26 2008 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Mon Nov 17 17:00:27 2008 +0100
     1.3 @@ -63,7 +63,7 @@
     1.4  (** auxiliary **)
     1.5  
     1.6  fun prove_interpretation tac prfx_atts expr inst =
     1.7 -  Locale.interpretation_i I prfx_atts expr inst
     1.8 +  Locale.interpretation I prfx_atts expr inst
     1.9    ##> Proof.global_terminal_proof
    1.10        (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (tac ctxt), Position.none), NONE)
    1.11    ##> ProofContext.theory_of;
    1.12 @@ -77,8 +77,11 @@
    1.13  
    1.14  val class_prefix = Logic.const_of_class o Sign.base_name;
    1.15  
    1.16 +fun class_name_morphism class =
    1.17 +  Name.map_prefix (K (Name.add_prefix false (class_prefix class)));
    1.18 +
    1.19  fun activate_class_morphism thy class inst morphism =
    1.20 -  Locale.get_interpret_morph thy class (false, class_prefix class) "" morphism class inst;
    1.21 +  Locale.get_interpret_morph thy (class_name_morphism class) (class, "") morphism class inst;
    1.22  
    1.23  fun prove_class_interpretation class inst consts hyp_facts def_facts thy =
    1.24    let
    1.25 @@ -92,7 +95,7 @@
    1.26    in
    1.27      thy
    1.28      |> fold2 add_constraint (map snd consts) no_constraints
    1.29 -    |> prove_interpretation tac (false, prfx) (Locale.Locale class)
    1.30 +    |> prove_interpretation tac (class_name_morphism class) (Locale.Locale class)
    1.31            (map SOME inst, map (pair (Attrib.no_binding) o Thm.prop_of) def_facts)
    1.32      ||> fold2 add_constraint (map snd consts) constraints
    1.33    end;
    1.34 @@ -621,7 +624,7 @@
    1.35      val supconsts = map (apsnd fst o snd) (these_params thy sups);
    1.36    in
    1.37      thy
    1.38 -    |> Locale.add_locale_i "" bname mergeexpr elems
    1.39 +    |> Locale.add_locale "" bname mergeexpr elems
    1.40      |> snd
    1.41      |> ProofContext.theory_of
    1.42      |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
     2.1 --- a/src/Pure/Isar/locale.ML	Mon Nov 17 17:00:26 2008 +0100
     2.2 +++ b/src/Pure/Isar/locale.ML	Mon Nov 17 17:00:27 2008 +0100
     2.3 @@ -63,10 +63,10 @@
     2.4    val declarations_of: theory -> string -> declaration list * declaration list;
     2.5  
     2.6    (* Processing of locale statements *)
     2.7 -  val read_context_statement: xstring option -> Element.context list ->
     2.8 +  val read_context_statement: string option -> Element.context list ->
     2.9      (string * string list) list list -> Proof.context ->
    2.10      string option * Proof.context * Proof.context * (term * term list) list list
    2.11 -  val read_context_statement_i: string option -> Element.context list ->
    2.12 +  val read_context_statement_cmd: xstring option -> Element.context list ->
    2.13      (string * string list) list list -> Proof.context ->
    2.14      string option * Proof.context * Proof.context * (term * term list) list list
    2.15    val cert_context_statement: string option -> Element.context_i list ->
    2.16 @@ -82,9 +82,9 @@
    2.17    val print_locale: theory -> bool -> expr -> Element.context list -> unit
    2.18    val print_registrations: bool -> string -> Proof.context -> unit
    2.19  
    2.20 -  val add_locale: string -> bstring -> expr -> Element.context list -> theory
    2.21 +  val add_locale: string -> bstring -> expr -> Element.context_i list -> theory
    2.22      -> string * Proof.context
    2.23 -  val add_locale_i: string -> bstring -> expr -> Element.context_i list -> theory
    2.24 +  val add_locale_cmd: bstring -> expr -> Element.context list -> theory
    2.25      -> string * Proof.context
    2.26  
    2.27    (* Tactics *)
    2.28 @@ -101,31 +101,25 @@
    2.29    val add_declaration: string -> declaration -> Proof.context -> Proof.context
    2.30  
    2.31    (* Interpretation *)
    2.32 -  val get_interpret_morph: theory -> string -> bool * string -> string ->
    2.33 +  val get_interpret_morph: theory -> (Name.binding -> Name.binding) -> string * string ->
    2.34      (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
    2.35      string -> term list -> Morphism.morphism
    2.36 -  val interpretation_i: (Proof.context -> Proof.context) ->
    2.37 -    bool * string -> expr ->
    2.38 +  val interpretation: (Proof.context -> Proof.context) ->
    2.39 +    (Name.binding -> Name.binding) -> expr ->
    2.40      term option list * (Attrib.binding * term) list ->
    2.41      theory ->
    2.42      (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
    2.43 -  val interpretation: (Proof.context -> Proof.context) ->
    2.44 -    bool * string -> expr ->
    2.45 -    string option list * (Attrib.binding * string) list ->
    2.46 -    theory ->
    2.47 -    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
    2.48 +  val interpretation_cmd: string -> expr -> string option list * (Attrib.binding * string) list ->
    2.49 +    theory -> Proof.state
    2.50    val interpretation_in_locale: (Proof.context -> Proof.context) ->
    2.51      xstring * expr -> theory -> Proof.state
    2.52 -  val interpret_i: (Proof.state -> Proof.state Seq.seq) ->
    2.53 -    bool * string -> expr ->
    2.54 +  val interpret: (Proof.state -> Proof.state Seq.seq) ->
    2.55 +    (Name.binding -> Name.binding) -> expr ->
    2.56      term option list * (Attrib.binding * term) list ->
    2.57      bool -> Proof.state ->
    2.58      (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
    2.59 -  val interpret: (Proof.state -> Proof.state Seq.seq) ->
    2.60 -    bool * string -> expr ->
    2.61 -    string option list * (Attrib.binding * string) list ->
    2.62 -    bool -> Proof.state ->
    2.63 -    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
    2.64 +  val interpret_cmd: string -> expr -> string option list * (Attrib.binding * string) list ->
    2.65 +    bool -> Proof.state -> Proof.state
    2.66  end;
    2.67  
    2.68  structure Locale: LOCALE =
    2.69 @@ -237,10 +231,8 @@
    2.70  (** management of registrations in theories and proof contexts **)
    2.71  
    2.72  type registration =
    2.73 -  {prfx: (bool * string) * string,
    2.74 -      (* first component: interpretation prefix;
    2.75 -           if the Boolean flag is set, only accesses containing the prefix are generated,
    2.76 -           otherwise the prefix may be omitted when accessing theorems etc.)
    2.77 +  {prfx: (Name.binding -> Name.binding) * (string * string),
    2.78 +      (* first component: interpretation name morphism;
    2.79           second component: parameter prefix *)
    2.80      exp: Morphism.morphism,
    2.81        (* maps content to its originating context *)
    2.82 @@ -261,18 +253,18 @@
    2.83      val join: T * T -> T
    2.84      val dest: theory -> T ->
    2.85        (term list *
    2.86 -        (((bool * string) * string) *
    2.87 +        (((Name.binding -> Name.binding) * (string * string)) *
    2.88           (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) *
    2.89           Element.witness list *
    2.90           thm Termtab.table)) list
    2.91      val test: theory -> T * term list -> bool
    2.92      val lookup: theory ->
    2.93        T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
    2.94 -      (((bool * string) * string) * Element.witness list * thm Termtab.table) option
    2.95 -    val insert: theory -> term list -> ((bool * string) * string) ->
    2.96 +      (((Name.binding -> Name.binding) * (string * string)) * Element.witness list * thm Termtab.table) option
    2.97 +    val insert: theory -> term list -> ((Name.binding -> Name.binding) * (string * string)) ->
    2.98        (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
    2.99        T ->
   2.100 -      T * (term list * (((bool * string) * string) * Element.witness list)) list
   2.101 +      T * (term list * (((Name.binding -> Name.binding) * (string * string)) * Element.witness list)) list
   2.102      val add_witness: term list -> Element.witness -> T -> T
   2.103      val add_equation: term list -> thm -> T -> T
   2.104  (*
   2.105 @@ -511,7 +503,7 @@
   2.106                  ("Subsumed interpretation(s) of locale " ^
   2.107                   quote (extern thy name) ^
   2.108                   "\nwith the following prefix(es):" ^
   2.109 -                  commas_quote (map (fn (_, ((_, s), _)) => s) sups))
   2.110 +                  commas_quote (map (fn (_, ((_, (_, s)), _)) => s) sups))
   2.111                else ();
   2.112      in Symtab.update (name, reg') regs end) ctxt;
   2.113  
   2.114 @@ -520,7 +512,6 @@
   2.115  fun put_local_registration id prfx morphs =
   2.116    Context.proof_map (put_registration id prfx morphs);
   2.117  
   2.118 -
   2.119  fun put_registration_in_locale name id =
   2.120    change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) =>
   2.121      (axiom, elems, params, decls, regs @ [(id, [])], intros, dests));
   2.122 @@ -585,16 +576,10 @@
   2.123      fun prt_witns [] = Pretty.str "no witnesses."
   2.124        | prt_witns witns = Pretty.block (Pretty.str "witnesses:" :: Pretty.brk 1 ::
   2.125            Pretty.breaks (map (Element.pretty_witness ctxt) witns))
   2.126 -    fun prt_reg (ts, ((_, ""), _, witns, eqns)) =
   2.127 +    fun prt_reg (ts, (_, _, witns, eqns)) =
   2.128          if show_wits
   2.129            then Pretty.block (prt_core ts eqns @ [Pretty.fbrk, prt_witns witns])
   2.130            else Pretty.block (prt_core ts eqns)
   2.131 -      | prt_reg (ts, (prfx, _, witns, eqns)) =
   2.132 -        if show_wits
   2.133 -          then Pretty.block ((prt_prfx prfx @ [Pretty.str ":", Pretty.brk 1] @
   2.134 -            prt_core ts eqns @ [Pretty.fbrk, prt_witns witns]))
   2.135 -          else Pretty.block ((prt_prfx prfx @
   2.136 -            [Pretty.str ":", Pretty.brk 1] @ prt_core ts eqns));
   2.137  
   2.138      val loc_int = intern thy loc;
   2.139      val regs = RegistrationsData.get (Context.Proof ctxt);
   2.140 @@ -604,7 +589,7 @@
   2.141          NONE => Pretty.str ("no interpretations")
   2.142        | SOME r => let
   2.143              val r' = Registrations.dest thy r;
   2.144 -            val r'' = Library.sort_wrt (fn (_, ((_, prfx), _, _, _)) => prfx) r';
   2.145 +            val r'' = Library.sort_wrt (fn (_, ((_, (_, prfx)), _, _, _)) => prfx) r';
   2.146            in Pretty.big_list ("interpretations:") (map prt_reg r'') end)
   2.147      |> Pretty.writeln
   2.148    end;
   2.149 @@ -676,7 +661,7 @@
   2.150  fun params_of' elemss =
   2.151    distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
   2.152  
   2.153 -fun param_prefix params = space_implode "_" params;
   2.154 +fun param_prefix locale_name params = (NameSpace.base locale_name, space_implode "_" params);
   2.155  
   2.156  
   2.157  (* CB: param_types has the following type:
   2.158 @@ -969,9 +954,12 @@
   2.159          val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode;
   2.160          val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
   2.161          val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
   2.162 +        val (locale_name, pprfx) = param_prefix name params;
   2.163 +        val add_prefices = pprfx <> "" ? Name.add_prefix false pprfx
   2.164 +          #> Name.add_prefix false locale_name;
   2.165          val elem_morphism =
   2.166            Element.rename_morphism ren $>
   2.167 -          Morphism.name_morphism (Name.add_prefix false (param_prefix params)) $>
   2.168 +          Morphism.name_morphism add_prefices $>
   2.169            Element.instT_morphism thy env;
   2.170          val elems' = map (Element.morph_ctxt elem_morphism) elems;
   2.171        in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
   2.172 @@ -1044,7 +1032,7 @@
   2.173                val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
   2.174              in if test_local_registration ctxt' (name, ps') then ctxt'
   2.175                else let
   2.176 -                  val ctxt'' = put_local_registration (name, ps') ((true, ""), "")
   2.177 +                  val ctxt'' = put_local_registration (name, ps') (I, (NameSpace.base name, ""))
   2.178                      (Morphism.identity, ((Vartab.empty, []), (Vartab.empty, []) )) ctxt'
   2.179                  in case mode of
   2.180                      Assumed axs =>
   2.181 @@ -1582,8 +1570,8 @@
   2.182  val read_expr = prep_expr read_context;
   2.183  val cert_expr = prep_expr cert_context;
   2.184  
   2.185 -fun read_context_statement loc = prep_statement intern read_ctxt loc;
   2.186 -fun read_context_statement_i loc = prep_statement (K I) read_ctxt loc;
   2.187 +fun read_context_statement loc = prep_statement (K I) read_ctxt loc;
   2.188 +fun read_context_statement_cmd loc = prep_statement intern read_ctxt loc;
   2.189  fun cert_context_statement loc = prep_statement (K I) cert_ctxt loc;
   2.190  
   2.191  end;
   2.192 @@ -1652,14 +1640,15 @@
   2.193  
   2.194  (* compute and apply morphism *)
   2.195  
   2.196 -fun add_prefixes loc (sticky, interp_prfx) param_prfx binding =
   2.197 +fun name_morph phi_name (locale_name, pprfx) binding =
   2.198    binding
   2.199 -  |> (if sticky andalso not (Name.is_nothing binding) andalso param_prfx <> ""
   2.200 -        then Name.add_prefix false param_prfx else I)
   2.201 -  |> Name.add_prefix sticky interp_prfx
   2.202 -  |> Name.add_prefix false (NameSpace.base loc ^ "_locale");
   2.203 -
   2.204 -fun inst_morph thy loc (sticky, interp_prfx) param_prfx insts prems eqns export =
   2.205 +  |> (if not (Name.is_nothing binding) andalso pprfx <> ""
   2.206 +        then Name.add_prefix false pprfx else I)
   2.207 +  |> (if not (Name.is_nothing binding)
   2.208 +        then Name.add_prefix false (locale_name ^ "_locale") else I)
   2.209 +  |> phi_name;
   2.210 +
   2.211 +fun inst_morph thy phi_name param_prfx insts prems eqns export =
   2.212    let
   2.213      (* standardise export morphism *)
   2.214      val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
   2.215 @@ -1669,29 +1658,30 @@
   2.216      val export' =
   2.217        Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
   2.218    in
   2.219 -    Morphism.name_morphism (add_prefixes loc (sticky, interp_prfx) param_prfx) $>
   2.220 -      Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
   2.221 +    Morphism.name_morphism (name_morph phi_name param_prfx) $>
   2.222 +      Element.inst_morphism thy insts $>
   2.223 +      Element.satisfy_morphism prems $>
   2.224        Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
   2.225        Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns) $>
   2.226        export'
   2.227    end;
   2.228  
   2.229 -fun activate_note thy loc (sticky, interp_prfx) param_prfx attrib insts prems eqns exp =
   2.230 +fun activate_note thy phi_name param_prfx attrib insts prems eqns exp =
   2.231    (Element.facts_map o Element.morph_ctxt)
   2.232 -      (inst_morph thy loc (sticky, interp_prfx) param_prfx insts prems eqns exp)
   2.233 +      (inst_morph thy phi_name param_prfx insts prems eqns exp)
   2.234    #> Attrib.map_facts attrib;
   2.235  
   2.236  
   2.237  (* public interface to interpretation morphism *)
   2.238  
   2.239 -fun get_interpret_morph thy loc (sticky, interp_prfx) param_prfx (exp, imp) target ext_ts =
   2.240 +fun get_interpret_morph thy phi_name param_prfx (exp, imp) target ext_ts =
   2.241    let
   2.242      val parms = the_locale thy target |> #params |> map fst;
   2.243      val ids = flatten (ProofContext.init thy, intern_expr thy)
   2.244        (([], Symtab.empty), Expr (Locale target)) |> fst |> fst;
   2.245      val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
   2.246    in
   2.247 -    inst_morph thy loc (sticky, interp_prfx) param_prfx insts prems eqns exp
   2.248 +    inst_morph thy phi_name param_prfx insts prems eqns exp
   2.249    end;
   2.250  
   2.251  (* store instantiations of args for all registered interpretations
   2.252 @@ -1706,11 +1696,11 @@
   2.253      val regs = get_global_registrations thy target;
   2.254      (* add args to thy for all registrations *)
   2.255  
   2.256 -    fun activate (ext_ts, (((sticky, interp_prfx), param_prfx), (exp, imp), _, _)) thy =
   2.257 +    fun activate (ext_ts, ((phi_name, param_prfx), (exp, imp), _, _)) thy =
   2.258        let
   2.259          val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
   2.260          val args' = args
   2.261 -          |> activate_note thy target (sticky, interp_prfx) param_prfx
   2.262 +          |> activate_note thy phi_name param_prfx
   2.263                 (Attrib.attribute_i thy) insts prems eqns exp;
   2.264        in
   2.265          thy
   2.266 @@ -2015,15 +2005,15 @@
   2.267  
   2.268  in
   2.269  
   2.270 -val add_locale = gen_add_locale read_context intern_expr;
   2.271 -val add_locale_i = gen_add_locale cert_context (K I);
   2.272 +val add_locale = gen_add_locale cert_context (K I);
   2.273 +val add_locale_cmd = gen_add_locale read_context intern_expr "";
   2.274  
   2.275  end;
   2.276  
   2.277  val _ = Context.>> (Context.map_theory
   2.278 - (add_locale_i "" "var" empty [Fixes [(Name.binding (Name.internal "x"), NONE, NoSyn)]] #>
   2.279 + (add_locale "" "var" empty [Fixes [(Name.binding (Name.internal "x"), NONE, NoSyn)]] #>
   2.280    snd #> ProofContext.theory_of #>
   2.281 -  add_locale_i "" "struct" empty [Fixes [(Name.binding (Name.internal "S"), NONE, Structure)]] #>
   2.282 +  add_locale "" "struct" empty [Fixes [(Name.binding (Name.internal "S"), NONE, Structure)]] #>
   2.283    snd #> ProofContext.theory_of));
   2.284  
   2.285  
   2.286 @@ -2032,7 +2022,7 @@
   2.287  (** Normalisation of locale statements ---
   2.288      discharges goals implied by interpretations **)
   2.289  
   2.290 -local
   2.291 +                                    local
   2.292  
   2.293  fun locale_assm_intros thy =
   2.294    Symtab.fold (fn (_, {intros = (a, _), ...}) => fn intros => (a @ intros))
   2.295 @@ -2086,7 +2076,7 @@
   2.296  (* activate instantiated facts in theory or context *)
   2.297  
   2.298  fun gen_activate_facts_elemss mk_ctxt note attrib put_reg add_wit add_eqn
   2.299 -        prfx all_elemss pss propss eq_attns (exp, imp) thmss thy_ctxt =
   2.300 +        phi_name all_elemss pss propss eq_attns (exp, imp) thmss thy_ctxt =
   2.301    let
   2.302      val ctxt = mk_ctxt thy_ctxt;
   2.303      fun get_reg thy_ctxt = get_local_registration (mk_ctxt thy_ctxt);
   2.304 @@ -2104,12 +2094,13 @@
   2.305  
   2.306      val thy_ctxt' = thy_ctxt
   2.307        (* add registrations *)
   2.308 -      |> fold (fn (((id, _), _), ps) => put_reg id (prfx, param_prefix ps) (exp, imp)) (new_elemss ~~ new_pss)
   2.309 +      |> fold2 (fn ((id as (loc, _), _), _) => fn ps => put_reg id (phi_name, param_prefix loc ps) (exp, imp))
   2.310 +           new_elemss new_pss
   2.311        (* add witnesses of Assumed elements (only those generate proof obligations) *)
   2.312 -      |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst new_propss ~~ new_thmss)
   2.313 +      |> fold2 (fn (id, _) => fold (add_wit id)) new_propss new_thmss
   2.314        (* add equations *)
   2.315 -      |> fold (fn (id, thms) => fold (add_eqn id) thms) (map fst eq_props ~~
   2.316 -          (map o map) (Drule.abs_def o LocalDefs.meta_rewrite_rule ctxt o
   2.317 +      |> fold2 (fn (id, _) => fold (add_eqn id)) eq_props
   2.318 +          ((map o map) (Drule.abs_def o LocalDefs.meta_rewrite_rule ctxt o
   2.319              Element.conclude_witness) eq_thms);
   2.320  
   2.321      val prems = flat (map_filter
   2.322 @@ -2118,22 +2109,23 @@
   2.323  
   2.324      val thy_ctxt'' = thy_ctxt'
   2.325        (* add witnesses of Derived elements *)
   2.326 -      |> fold (fn (id, thms) => fold (add_wit id o Element.morph_witness (Element.satisfy_morphism prems)) thms)
   2.327 +      |> fold (fn (id, thms) => fold
   2.328 +           (add_wit id o Element.morph_witness (Element.satisfy_morphism prems)) thms)
   2.329           (map_filter (fn ((_, Assumed _), _) => NONE
   2.330              | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
   2.331  
   2.332 -    fun activate_elem loc (sticky, interp_prfx) param_prfx insts prems eqns exp (Notes (kind, facts)) thy_ctxt =
   2.333 +    fun activate_elem phi_name param_prfx insts prems eqns exp (Notes (kind, facts)) thy_ctxt =
   2.334          let
   2.335            val ctxt = mk_ctxt thy_ctxt;
   2.336            val thy = ProofContext.theory_of ctxt;
   2.337            val facts' = facts
   2.338 -            |> activate_note thy loc (sticky, interp_prfx) param_prfx
   2.339 +            |> activate_note thy phi_name param_prfx
   2.340                   (attrib thy_ctxt) insts prems eqns exp;
   2.341          in 
   2.342            thy_ctxt
   2.343            |> fold (snd oo note kind) facts'
   2.344          end
   2.345 -      | activate_elem _ _ _ _ _ _ _ _ thy_ctxt = thy_ctxt;
   2.346 +      | activate_elem _ _ _ _ _ _ _ thy_ctxt = thy_ctxt;
   2.347  
   2.348      fun activate_elems (((loc, ext_ts), _), _) ps thy_ctxt =
   2.349        let
   2.350 @@ -2141,13 +2133,13 @@
   2.351          val thy = ProofContext.theory_of ctxt;
   2.352          val {params, elems, ...} = the_locale thy loc;
   2.353          val parms = map fst params;
   2.354 -        val param_prfx = param_prefix ps;
   2.355 +        val param_prfx = param_prefix loc ps;
   2.356          val ids = flatten (ProofContext.init thy, intern_expr thy)
   2.357            (([], Symtab.empty), Expr (Locale loc)) |> fst |> fst;
   2.358          val (insts, prems, eqns) = collect_witnesses ctxt imp parms ids ext_ts;
   2.359        in
   2.360          thy_ctxt
   2.361 -        |> fold (activate_elem loc prfx param_prfx insts prems eqns exp o fst) elems
   2.362 +        |> fold (activate_elem phi_name param_prfx insts prems eqns exp o fst) elems
   2.363        end;
   2.364  
   2.365    in
   2.366 @@ -2236,7 +2228,7 @@
   2.367  
   2.368  fun gen_prep_registration mk_ctxt test_reg activate
   2.369      prep_attr prep_expr prep_insts
   2.370 -    thy_ctxt prfx raw_expr raw_insts =
   2.371 +    thy_ctxt phi_name raw_expr raw_insts =
   2.372    let
   2.373      val ctxt = mk_ctxt thy_ctxt;
   2.374      val thy = ProofContext.theory_of ctxt;
   2.375 @@ -2301,7 +2293,7 @@
   2.376      val propss = map extract_asms_elems inst_elemss @ eqn_elems;
   2.377  
   2.378    in
   2.379 -    (propss, activate prfx inst_elemss (map (snd o fst) ids) propss eq_attns morphs, morphs)
   2.380 +    (propss, activate phi_name inst_elemss (map (snd o fst) ids) propss eq_attns morphs, morphs)
   2.381    end;
   2.382  
   2.383  fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init
   2.384 @@ -2313,14 +2305,14 @@
   2.385    local_activate_facts_elemss mk_ctxt;
   2.386  
   2.387  val prep_global_registration = gen_prep_global_registration
   2.388 +  (K I) (K I) check_instantiations;
   2.389 +val prep_global_registration_cmd = gen_prep_global_registration
   2.390    Attrib.intern_src intern_expr read_instantiations;
   2.391 -val prep_global_registration_i = gen_prep_global_registration
   2.392 -  (K I) (K I) check_instantiations;
   2.393  
   2.394  val prep_local_registration = gen_prep_local_registration
   2.395 +  (K I) (K I) check_instantiations;
   2.396 +val prep_local_registration_cmd = gen_prep_local_registration
   2.397    Attrib.intern_src intern_expr read_instantiations;
   2.398 -val prep_local_registration_i = gen_prep_local_registration
   2.399 -  (K I) (K I) check_instantiations;
   2.400  
   2.401  fun prep_registration_in_locale target expr thy =
   2.402    (* target already in internal form *)
   2.403 @@ -2362,7 +2354,7 @@
   2.404                  |> fold (add_witness_in_locale target id) thms
   2.405            | activate_id _ thy = thy;
   2.406  
   2.407 -        fun activate_reg (ext_ts, (((sticky, interp_prfx), param_prfx), (exp, imp), _, _)) thy =
   2.408 +        fun activate_reg (ext_ts, ((phi_name, param_prfx), (exp, imp), _, _)) thy =
   2.409            let
   2.410              val (insts, wits, _) = collect_witnesses (ProofContext.init thy) imp fixed target_ids ext_ts;
   2.411              val inst_parms = map (the o AList.lookup (op =) (map #1 fixed ~~ ext_ts));
   2.412 @@ -2376,7 +2368,7 @@
   2.413                  if test_global_registration thy (name, ps')
   2.414                  then thy
   2.415                  else thy
   2.416 -                  |> put_global_registration (name, ps') ((sticky, interp_prfx), param_prefix ps) (exp, imp)
   2.417 +                  |> put_global_registration (name, ps') (phi_name, param_prefix name ps) (exp, imp)
   2.418                    |> fold (fn witn => fn thy => add_global_witness (name, ps')
   2.419                       (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms
   2.420                end;
   2.421 @@ -2388,7 +2380,7 @@
   2.422                  if test_global_registration thy (name, ps')
   2.423                  then thy
   2.424                  else thy
   2.425 -                  |> put_global_registration (name, ps') ((sticky, interp_prfx), param_prefix ps) (exp, imp)
   2.426 +                  |> put_global_registration (name, ps') (phi_name, param_prefix name ps) (exp, imp)
   2.427                    |> fold (fn witn => fn thy => add_global_witness (name, ps')
   2.428                         (witn |> Element.map_witness (fn (t, th) =>  (* FIXME *)
   2.429                         (Element.inst_term insts t,
   2.430 @@ -2398,14 +2390,14 @@
   2.431              fun activate_elem (loc, ps) (Notes (kind, facts)) thy =
   2.432                  let
   2.433                    val att_morphism =
   2.434 -                    Morphism.name_morphism (add_prefixes loc (sticky, interp_prfx) param_prfx) $>
   2.435 +                    Morphism.name_morphism (name_morph phi_name param_prfx) $>
   2.436                      Morphism.thm_morphism satisfy $>
   2.437                      Element.inst_morphism thy insts $>
   2.438                      Morphism.thm_morphism disch;
   2.439                    val facts' = facts
   2.440                      |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism)
   2.441                      |> (map o apsnd o map o apfst o map) (disch o Element.inst_thm thy insts o satisfy)
   2.442 -                    |> (map o apfst o apfst) (add_prefixes loc (sticky, interp_prfx) param_prfx);
   2.443 +                    |> (map o apfst o apfst) (name_morph phi_name param_prfx);
   2.444                  in
   2.445                    thy
   2.446                    |> fold (snd oo global_note_prefix kind) facts'
   2.447 @@ -2446,12 +2438,11 @@
   2.448      |> pair morphs
   2.449    end;
   2.450  
   2.451 -fun gen_interpret prep_registration after_qed prfx expr insts int state =
   2.452 -  (* prfx = (flag indicating full qualification, name prefix) *)
   2.453 +fun gen_interpret prep_registration after_qed name_morph expr insts int state =
   2.454    let
   2.455      val _ = Proof.assert_forward_or_chain state;
   2.456      val ctxt = Proof.context_of state;
   2.457 -    val (propss, activate, morphs) = prep_registration ctxt prfx expr insts;
   2.458 +    val (propss, activate, morphs) = prep_registration ctxt name_morph expr insts;
   2.459      fun after_qed' results =
   2.460        Proof.map_context (K (ctxt |> activate (prep_result propss results)))
   2.461        #> Proof.put_facts NONE
   2.462 @@ -2464,11 +2455,19 @@
   2.463      |> pair morphs
   2.464    end;
   2.465  
   2.466 +fun standard_name_morph interp_prfx binding =
   2.467 +  if Name.is_nothing binding then binding
   2.468 +  else Name.map_prefix (fn ((locale_name, _) :: pprfx) =>
   2.469 +    fold (Name.add_prefix false o fst) pprfx
   2.470 +    #> interp_prfx <> "" ? Name.add_prefix true interp_prfx
   2.471 +    #> Name.add_prefix false locale_name
   2.472 +  ) binding;
   2.473 +
   2.474  in
   2.475  
   2.476 -val interpretation_i = gen_interpretation prep_global_registration_i;
   2.477  val interpretation = gen_interpretation prep_global_registration;
   2.478 -
   2.479 +fun interpretation_cmd interp_prfx = snd ooo gen_interpretation prep_global_registration_cmd
   2.480 +  I (standard_name_morph interp_prfx);
   2.481  
   2.482  fun interpretation_in_locale after_qed (raw_target, expr) thy =
   2.483    let
   2.484 @@ -2489,8 +2488,9 @@
   2.485      |> Element.refine_witness |> Seq.hd
   2.486    end;
   2.487  
   2.488 -val interpret_i = gen_interpret prep_local_registration_i;
   2.489  val interpret = gen_interpret prep_local_registration;
   2.490 +fun interpret_cmd interp_prfx = snd oooo gen_interpret prep_local_registration_cmd
   2.491 +  Seq.single (standard_name_morph interp_prfx);
   2.492  
   2.493  end;
   2.494  
     3.1 --- a/src/Pure/Isar/theory_target.ML	Mon Nov 17 17:00:26 2008 +0100
     3.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Nov 17 17:00:27 2008 +0100
     3.3 @@ -186,7 +186,7 @@
     3.4    let
     3.5      val c' = Morphism.name phi c;
     3.6      val rhs' = Morphism.term phi rhs;
     3.7 -    val name' = Name.name_of c';
     3.8 +    val name' = Name.name_with_prefix c';
     3.9      val legacy_arg = (name', Term.close_schematic_term (Logic.legacy_varify rhs'));
    3.10      val arg = (name', Term.close_schematic_term rhs');
    3.11      val similar_body = Type.similar_types (rhs, rhs');
    3.12 @@ -197,7 +197,10 @@
    3.13    in
    3.14      not (is_class andalso (similar_body orelse class_global)) ?
    3.15        (Context.mapping_result
    3.16 -        (Sign.add_abbrev PrintMode.internal tags legacy_arg)
    3.17 +        (fn thy => thy |> 
    3.18 +          Sign.no_base_names
    3.19 +          |> Sign.add_abbrev PrintMode.internal tags legacy_arg
    3.20 +          ||> Sign.restore_naming thy)
    3.21          (ProofContext.add_abbrev PrintMode.internal tags arg)
    3.22        #-> (fn (lhs' as Const (d, _), _) =>
    3.23            similar_body ?