# HG changeset patch
# User wenzelm
# Date 1236782740 -3600
# Node ID 910a7aeb8dec0ac29b5a876c9db8948923128a5a
# Parent  0e3c88f132fc63fcbe0164334b616fb5797f6786
more precise treatment of qualified bindings;
tuned;

diff -r 0e3c88f132fc -r 910a7aeb8dec src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Wed Mar 11 15:44:12 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Wed Mar 11 15:45:40 2009 +0100
@@ -1,5 +1,6 @@
 (*  Title:      Pure/Isar/theory_target.ML
     Author:     Makarius
+    Author:     Florian Haftmann, TU Muenchen
 
 Common theory/locale/class/instantiation/overloading targets.
 *)
@@ -48,10 +49,10 @@
   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]);
@@ -195,8 +196,8 @@
   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)
@@ -210,7 +211,7 @@
 
 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;
@@ -278,8 +279,7 @@
     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' [];
@@ -290,6 +290,7 @@
     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) =>