src/Pure/Isar/theory_target.ML

 
 fun pretty_thy ctxt target is_locale is_class =
   let
     val thy = ProofContext.theory_of ctxt;
     val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
-    val fixes = map (fn (x, T) => (x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
-    val assumes = map (fn A => (("", []), [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt));
+    val fixes = map (fn (x, T) =>
+      (Name.binding x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
+    val assumes = map (fn A =>
+      ((Name.no_binding, []), [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt));
     val elems =
       (if null fixes then [] else [Element.Fixes fixes]) @
       (if null assumes then [] else [Element.Assumes assumes]);
   in
     if target = "" then []

     val (th'' :: vs) = (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees))
       |> Variable.export ctxt thy_ctxt
       |> Drule.zero_var_indexes_list;
 
     (*thm definition*)
-    val result = PureThy.name_thm true true name th'';
+    val result = PureThy.name_thm true true Position.none name th'';
 
     (*import fixes*)
     val (tvars, vars) =
       chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs)
       |>> map Logic.dest_type;

     val result'' =
       (case SINGLE (Seq.INTERVAL assm_tac 1 nprems) result' of
         NONE => raise THM ("Failed to re-import result", 0, [result'])
       | SOME res => LocalDefs.trans_props ctxt [res, Thm.symmetric concl_conv])
       |> Goal.norm_result
-      |> PureThy.name_thm false false name;
+      |> PureThy.name_thm false false Position.none name;
 
   in (result'', result) end;
 
 fun note_local kind facts ctxt =
   ctxt

   let
     val thy = ProofContext.theory_of lthy;
     val full = LocalTheory.full_name lthy;
 
     val facts' = facts
-      |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi (full (fst a))) bs))
+      |> map (fn (a, bs) =>
+        (a, PureThy.burrow_fact (PureThy.name_multi (full (Name.name_of (fst a)))) bs))
       |> PureThy.map_facts (import_export_proof lthy);
     val local_facts = PureThy.map_facts #1 facts'
       |> Attrib.map_facts (Attrib.attribute_i thy);
     val target_facts = PureThy.map_facts #1 facts'
       |> is_locale ? Element.facts_map (Element.morph_ctxt (LocalTheory.target_morphism lthy));

 
 fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((c, mx), rhs) phi =
   let
     val c' = Morphism.name phi c;
     val rhs' = Morphism.term phi rhs;
-    val legacy_arg = (c', Term.close_schematic_term (Logic.legacy_varify rhs'));
-    val arg = (c', Term.close_schematic_term rhs');
+    val name = Name.name_of c;
+    val name' = Name.name_of c'
+    val legacy_arg = (name', Term.close_schematic_term (Logic.legacy_varify rhs'));
+    val arg = (name', Term.close_schematic_term rhs');
     val similar_body = Type.similar_types (rhs, rhs');
     (* FIXME workaround based on educated guess *)
-    val class_global = c' = NameSpace.qualified (Class.class_prefix target) c;
+    val class_global = name' = NameSpace.qualified (Class.class_prefix target) name;
   in
     not (is_class andalso (similar_body orelse class_global)) ?
       (Context.mapping_result
         (Sign.add_abbrev PrintMode.internal tags legacy_arg)
         (ProofContext.add_abbrev PrintMode.internal tags arg)

           similar_body ?
             (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
              Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
   end;
 
-fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((c, T), mx) lthy =
-  let
+fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
+  let
+    val c = Name.name_of b;
     val tags = LocalTheory.group_position_of lthy;
     val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
     val U = map #2 xs ---> T;
     val (mx1, mx2, mx3) = fork_mixfix ta mx;
     fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);

             | NONE => LocalTheory.theory_result (Sign.declare_const tags (c, U, mx3))));
     val (const, lthy') = lthy |> declare_const;
     val t = Term.list_comb (const, map Free xs);
   in
     lthy'
-    |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default tags ((c, mx2), t))
+    |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default tags ((b, mx2), t))
     |> is_class ? class_target ta (Class.declare target tags ((c, mx1), t))
-    |> LocalDefs.add_def ((c, NoSyn), t)
+    |> LocalDefs.add_def ((b, NoSyn), t)
   end;
 
 
 (* abbrev *)
 
-fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((c, mx), t) lthy =
-  let
+fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
+  let
+    val c = Name.name_of b;
     val tags = LocalTheory.group_position_of lthy;
     val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
     val target_ctxt = LocalTheory.target_of lthy;
 
     val (mx1, mx2, mx3) = fork_mixfix ta mx;

     lthy |>
      (if is_locale then
         LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal tags (c, global_rhs))
         #-> (fn (lhs, _) =>
           let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
-            term_syntax ta (locale_const ta prmode tags ((c, mx2), lhs')) #>
+            term_syntax ta (locale_const ta prmode tags ((b, mx2), lhs')) #>
             is_class ? class_target ta (Class.abbrev target prmode tags ((c, mx1), t'))
           end)
       else
         LocalTheory.theory
           (Sign.add_abbrev (#1 prmode) tags (c, global_rhs) #-> (fn (lhs, _) =>
            Sign.notation true prmode [(lhs, mx3)])))
     |> ProofContext.add_abbrev PrintMode.internal tags (c, t) |> snd
-    |> LocalDefs.fixed_abbrev ((c, NoSyn), t)
+    |> LocalDefs.fixed_abbrev ((b, NoSyn), t)
   end;
 
 
 (* define *)
 
 fun define (ta as Target {target, is_locale, is_class, ...})
-    kind ((c, mx), ((name, atts), rhs)) lthy =
+    kind ((b, mx), ((name, atts), rhs)) lthy =
   let
     val thy = ProofContext.theory_of lthy;
     val thy_ctxt = ProofContext.init thy;
 
-    val name' = Thm.def_name_optional c name;
+    val c = Name.name_of b;
+    val name' = Name.map_name (Thm.def_name_optional c) name;
     val (rhs', rhs_conv) =
       LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
     val xs = Variable.add_fixed (LocalTheory.target_of lthy) rhs' [];
     val T = Term.fastype_of rhs;
 
     (*const*)
-    val ((lhs, local_def), lthy2) = lthy |> declare_const ta (member (op =) xs) ((c, T), mx);
+    val ((lhs, local_def), lthy2) = lthy |> declare_const ta (member (op =) xs) ((b, T), mx);
     val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
 
     (*def*)
     val define_const =
       (case Overloading.operation lthy c of

       | NONE =>
           if is_none (Class.instantiation_param lthy c)
           then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
           else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
     val (global_def, lthy3) = lthy2
-      |> LocalTheory.theory_result (define_const name' (lhs', rhs'));
+      |> LocalTheory.theory_result (define_const (Name.name_of name') (lhs', rhs'));
     val def = LocalDefs.trans_terms lthy3
       [(*c == global.c xs*)     local_def,
        (*global.c xs == rhs'*)  global_def,
        (*rhs' == rhs*)          Thm.symmetric rhs_conv];
 

     val global_consts = map (Term.dest_Const o Term.head_of o Thm.term_of o Thm.rhs_of o #2) consts;
 
     (*axioms*)
     val hyps = map Thm.term_of (Assumption.assms_of lthy');
     fun axiom ((name, atts), props) thy = thy
-      |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi name props)
+      |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi (Name.name_of name) props)
       |-> (fn ths => pair ((name, atts), [(ths, [])]));
   in
     lthy'
     |> fold Variable.declare_term expanded_props
     |> LocalTheory.theory (fold (fn c => Theory.add_deps "" c []) global_consts)