Binding.str_of: removed verbose feature, include qualifier in output;
renamed Binding.add_prefix to Binding.prefix;

--- a/src/Pure/General/binding.ML	Sat Mar 07 11:31:41 2009 +0100
+++ b/src/Pure/General/binding.ML	Sat Mar 07 11:32:31 2009 +0100
@@ -11,7 +11,6 @@
 sig
   type binding
   val dest: binding -> (string * bool) list * bstring
-  val verbose: bool ref
   val str_of: binding -> string
   val make: bstring * Position.T -> binding
   val pos_of: binding -> Position.T
@@ -23,7 +22,7 @@
   val qualify: bool -> string -> binding -> binding
   val prefix_of: binding -> (string * bool) list
   val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
-  val add_prefix: bool -> string -> binding -> binding
+  val prefix: bool -> string -> binding -> binding
 end;
 
 structure Binding: BINDING =
@@ -47,20 +46,9 @@
 
 fun dest (Binding {prefix, qualifier, name, ...}) = (prefix @ qualifier, name);
 
-
-(* diagnostic output *)
-
-val verbose = ref false;
-
-val str_of_components = implode o map (fn (s, true) => s ^ "!" | (s, false) => s ^ "?");
-
 fun str_of (Binding {prefix, qualifier, name, pos}) =
   let
-    val text =
-      if ! verbose then
-        (if null prefix then "" else enclose "(" ")" (str_of_components prefix)) ^
-          str_of_components qualifier ^ name
-      else name;
+    val text = space_implode "." (map #1 qualifier @ [name]);
     val props = Position.properties_of pos;
   in Markup.markup (Markup.properties props (Markup.binding name)) text end;
 
@@ -85,8 +73,8 @@
 (* user qualifier *)
 
 fun qualify _ "" = I
-  | qualify mandatory qual = map_binding (fn (prefix, qualifier, name, pos) =>
-      (prefix, (qual, mandatory) :: qualifier, name, pos));
+  | qualify strict qual = map_binding (fn (prefix, qualifier, name, pos) =>
+      (prefix, (qual, strict) :: qualifier, name, pos));
 
 
 (* system prefix *)
@@ -96,8 +84,8 @@
 fun map_prefix f = map_binding (fn (prefix, qualifier, name, pos) =>
   (f prefix, qualifier, name, pos));
 
-fun add_prefix _ "" = I
-  | add_prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
+fun prefix _ "" = I
+  | prefix strict prfx = map_prefix (cons (prfx, strict));
 
 end;
 

--- a/src/Pure/Isar/class.ML	Sat Mar 07 11:31:41 2009 +0100
+++ b/src/Pure/Isar/class.ML	Sat Mar 07 11:32:31 2009 +0100
@@ -66,8 +66,7 @@
 
     (* canonical interpretation *)
     val base_morph = inst_morph
-      $> Morphism.binding_morphism
-           (Binding.add_prefix false (class_prefix class))
+      $> Morphism.binding_morphism (Binding.prefix false (class_prefix class))
       $> Element.satisfy_morphism (the_list wit);
     val defs = these_defs thy sups;
     val eq_morph = Element.eq_morphism thy defs;

--- a/src/Pure/Isar/expression.ML	Sat Mar 07 11:31:41 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Sat Mar 07 11:32:31 2009 +0100
@@ -186,7 +186,7 @@
     val inst = Symtab.make insts'';
   in
     (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
-      Morphism.binding_morphism (Binding.add_prefix strict prfx), ctxt')
+      Morphism.binding_morphism (Binding.prefix strict prfx), ctxt')
   end;