src/Pure/Isar/theory_target.ML

 (*  Title:      Pure/Isar/theory_target.ML
     Author:     Makarius
+    Author:     Florian Haftmann, TU Muenchen
 
 Common theory/locale/class/instantiation/overloading targets.
 *)
 
 signature THEORY_TARGET =

 
 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) => (Binding.name x, SOME T, NoSyn))
-      (#1 (ProofContext.inferred_fixes ctxt));
-    val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
-      (Assumption.assms_of ctxt);
+    val fixes =
+      map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
+    val assumes =
+      map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) (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 []

       andalso not (null prefix')
       andalso (fst o snd o split_last) prefix' = Class_Target.class_prefix target;
   in
     not (is_class andalso (similar_body orelse class_global)) ?
       (Context.mapping_result
-        (fn thy => thy |> 
-          Sign.no_base_names
+        (fn thy => thy
+          |> Sign.no_base_names
           |> Sign.add_abbrev PrintMode.internal tags legacy_arg
           ||> Sign.restore_naming thy)
         (ProofContext.add_abbrev PrintMode.internal tags arg)
       #-> (fn (lhs' as Const (d, _), _) =>
           similar_body ?

 
 fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
 
 fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
   let
-    val c = Binding.name_of b;  (* FIXME Binding.qualified_name_of *)
+    val c = Binding.qualified_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;
     val declare_const =

     kind ((b, mx), ((name, atts), rhs)) lthy =
   let
     val thy = ProofContext.theory_of lthy;
     val thy_ctxt = ProofContext.init thy;
 
-    val c = Binding.name_of b;   (* FIXME Binding.qualified_name_of (!?) *)
-    val name' = Binding.map_name (Thm.def_name_optional (Binding.name_of b)) name;
+    val name' = Thm.def_binding_optional b 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) ((b, T), mx);
     val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
 
     (*def*)
+    val c = Binding.qualified_name_of b;
     val define_const =
       (case Overloading.operation lthy c of
         SOME (_, checked) =>
           (fn name => fn (Const (c, _), rhs) => Overloading.define checked name (c, rhs))
       | NONE =>