new Binding module
authorhaftmann
Mon Dec 01 19:41:16 2008 +0100 (2008-12-01)
changeset 28941128459bd72d2
parent 28940 df0cb410be35
child 28942 043a42ba2a4d
new Binding module
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_set_package.ML
src/Pure/General/ROOT.ML
src/Pure/General/binding.ML
src/Pure/General/name_space.ML
src/Pure/Isar/args.ML
src/Pure/Isar/class.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/theory_target.ML
src/Pure/facts.ML
src/Pure/name.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Dec 01 16:02:57 2008 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Dec 01 19:41:16 2008 +0100
     1.3 @@ -638,8 +638,8 @@
     1.4      (* add definiton of recursive predicates to theory *)
     1.5  
     1.6      val rec_name =
     1.7 -      if Name.is_nothing alt_name then
     1.8 -        Name.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
     1.9 +      if Binding.is_nothing alt_name then
    1.10 +        Binding.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
    1.11        else alt_name;
    1.12  
    1.13      val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
     2.1 --- a/src/HOL/Tools/inductive_set_package.ML	Mon Dec 01 16:02:57 2008 +0100
     2.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Mon Dec 01 19:41:16 2008 +0100
     2.3 @@ -499,8 +499,8 @@
     2.4  
     2.5      (* convert theorems to set notation *)
     2.6      val rec_name =
     2.7 -      if Name.is_nothing alt_name then
     2.8 -        Name.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
     2.9 +      if Binding.is_nothing alt_name then
    2.10 +        Binding.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
    2.11        else alt_name;
    2.12      val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o Name.name_of o #1) cnames_syn;  (* FIXME *)
    2.13      val (intr_names, intr_atts) = split_list (map fst intros);
     3.1 --- a/src/Pure/General/ROOT.ML	Mon Dec 01 16:02:57 2008 +0100
     3.2 +++ b/src/Pure/General/ROOT.ML	Mon Dec 01 19:41:16 2008 +0100
     3.3 @@ -27,6 +27,7 @@
     3.4  use "ord_list.ML";
     3.5  use "balanced_tree.ML";
     3.6  use "graph.ML";
     3.7 +use "binding.ML";
     3.8  use "name_space.ML";
     3.9  use "lazy.ML";
    3.10  use "path.ML";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/General/binding.ML	Mon Dec 01 19:41:16 2008 +0100
     4.3 @@ -0,0 +1,75 @@
     4.4 +(*  Title:      Pure/General/binding.ML
     4.5 +    Author:     Florian Haftmann, TU Muenchen
     4.6 +
     4.7 +Structured name bindings.
     4.8 +*)
     4.9 +
    4.10 +signature BASIC_BINDING =
    4.11 +sig
    4.12 +  val long_names: bool ref
    4.13 +  val short_names: bool ref
    4.14 +  val unique_names: bool ref
    4.15 +end;
    4.16 +
    4.17 +signature BINDING =
    4.18 +sig
    4.19 +  include BASIC_BINDING
    4.20 +  type T
    4.21 +  val binding_pos: string * Position.T -> T
    4.22 +  val binding: string -> T
    4.23 +  val no_binding: T
    4.24 +  val dest_binding: T -> (string * bool) list * string
    4.25 +  val is_nothing: T -> bool
    4.26 +  val pos_of: T -> Position.T
    4.27 + 
    4.28 +  val map_binding: ((string * bool) list * string -> (string * bool) list * string)
    4.29 +    -> T -> T
    4.30 +  val add_prefix: bool -> string -> T -> T
    4.31 +  val map_prefix: ((string * bool) list -> T -> T) -> T -> T
    4.32 +  val display: T -> string
    4.33 +end
    4.34 +
    4.35 +structure Binding : BINDING =
    4.36 +struct
    4.37 +
    4.38 +(** global flags **)
    4.39 +
    4.40 +val long_names = ref false;
    4.41 +val short_names = ref false;
    4.42 +val unique_names = ref true;
    4.43 +
    4.44 +
    4.45 +(** binding representation **)
    4.46 +
    4.47 +datatype T = Binding of ((string * bool) list * string) * Position.T;
    4.48 +  (* (prefix components (with mandatory flag), base name, position) *)
    4.49 +
    4.50 +fun binding_pos (name, pos) = Binding (([], name), pos);
    4.51 +fun binding name = binding_pos (name, Position.none);
    4.52 +val no_binding = binding "";
    4.53 +
    4.54 +fun pos_of (Binding (_, pos)) = pos;
    4.55 +fun dest_binding (Binding (prefix_name, _)) = prefix_name;
    4.56 +
    4.57 +fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos);
    4.58 +
    4.59 +fun is_nothing (Binding ((_, name), _)) = name = "";
    4.60 +
    4.61 +fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix"
    4.62 +  else (map_binding o apfst) (cons (prfx, sticky)) b;
    4.63 +
    4.64 +fun map_prefix f (Binding ((prefix, name), pos)) =
    4.65 +  f prefix (binding_pos (name, pos));
    4.66 +
    4.67 +fun display (Binding ((prefix, name), _)) =
    4.68 +  let
    4.69 +    fun mk_prefix (prfx, true) = prfx
    4.70 +      | mk_prefix (prfx, false) = enclose "(" ")" prfx
    4.71 +  in if not (! long_names) orelse null prefix orelse name = "" then name
    4.72 +    else space_implode "." (map mk_prefix prefix) ^ ":" ^ name
    4.73 +  end;
    4.74 +
    4.75 +end;
    4.76 +
    4.77 +structure Basic_Binding : BASIC_BINDING = Binding;
    4.78 +open Basic_Binding;
     5.1 --- a/src/Pure/General/name_space.ML	Mon Dec 01 16:02:57 2008 +0100
     5.2 +++ b/src/Pure/General/name_space.ML	Mon Dec 01 19:41:16 2008 +0100
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      Pure/General/name_space.ML
     5.5 -    ID:         $Id$
     5.6      Author:     Markus Wenzel, TU Muenchen
     5.7  
     5.8  Generic name spaces with declared and hidden entries.  Unknown names
     5.9 @@ -9,29 +8,9 @@
    5.10  type bstring = string;    (*names to be bound*)
    5.11  type xstring = string;    (*external names*)
    5.12  
    5.13 -signature BASIC_NAME_SPACE =
    5.14 -sig
    5.15 -  val long_names: bool ref
    5.16 -  val short_names: bool ref
    5.17 -  val unique_names: bool ref
    5.18 -end;
    5.19 -
    5.20 -signature NAME_BINDING =
    5.21 -sig
    5.22 -  type binding
    5.23 -  val binding_pos: string * Position.T -> binding
    5.24 -  val binding: string -> binding
    5.25 -  val no_binding: binding
    5.26 -  val dest_binding: binding -> (string * bool) list * string
    5.27 -  val is_nothing: binding -> bool
    5.28 -  val pos_of: binding -> Position.T
    5.29 -  val map_binding: ((string * bool) list * string -> (string * bool) list * string)
    5.30 -    -> binding -> binding
    5.31 -end
    5.32 -
    5.33  signature NAME_SPACE =
    5.34  sig
    5.35 -  include BASIC_NAME_SPACE
    5.36 +  include BASIC_BINDING
    5.37    val hidden: string -> string
    5.38    val is_hidden: string -> bool
    5.39    val separator: string                 (*single char*)
    5.40 @@ -60,14 +39,13 @@
    5.41    val no_base_names: naming -> naming
    5.42    val qualified_names: naming -> naming
    5.43    val sticky_prefix: string -> naming -> naming
    5.44 -  include NAME_BINDING
    5.45 -  val full_binding: naming -> binding -> string
    5.46 -  val declare_binding: naming -> binding -> T -> string * T
    5.47 +  val full_binding: naming -> Binding.T -> string
    5.48 +  val declare_binding: naming -> Binding.T -> T -> string * T
    5.49    type 'a table = T * 'a Symtab.table
    5.50    val empty_table: 'a table
    5.51 -  val table_declare: naming -> binding * 'a
    5.52 +  val table_declare: naming -> Binding.T * 'a
    5.53      -> 'a table -> string * 'a table (*exception Symtab.DUP*)
    5.54 -  val table_declare_permissive: naming -> binding * 'a
    5.55 +  val table_declare_permissive: naming -> Binding.T * 'a
    5.56      -> 'a table -> string * 'a table
    5.57    val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
    5.58    val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
    5.59 @@ -78,6 +56,9 @@
    5.60  structure NameSpace: NAME_SPACE =
    5.61  struct
    5.62  
    5.63 +open Basic_Binding;
    5.64 +
    5.65 +
    5.66  (** long identifiers **)
    5.67  
    5.68  fun hidden name = "??." ^ name;
    5.69 @@ -170,10 +151,6 @@
    5.70  
    5.71  fun intern space xname = #1 (lookup space xname);
    5.72  
    5.73 -val long_names = ref false;
    5.74 -val short_names = ref false;
    5.75 -val unique_names = ref true;
    5.76 -
    5.77  fun extern space name =
    5.78    let
    5.79      fun valid unique xname =
    5.80 @@ -241,23 +218,6 @@
    5.81  
    5.82  
    5.83  
    5.84 -(** generic name bindings **)
    5.85 -
    5.86 -datatype binding = Binding of ((string * bool) list * string) * Position.T;
    5.87 -
    5.88 -fun binding_pos (name, pos) = Binding (([], name), pos);
    5.89 -fun binding name = binding_pos (name, Position.none);
    5.90 -val no_binding = binding "";
    5.91 -
    5.92 -fun pos_of (Binding (_, pos)) = pos;
    5.93 -fun dest_binding (Binding (prefix_name, _)) = prefix_name;
    5.94 -
    5.95 -fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos);
    5.96 -
    5.97 -fun is_nothing (Binding ((_, name), _)) = name = "";
    5.98 -
    5.99 -
   5.100 -
   5.101  (** naming contexts **)
   5.102  
   5.103  (* datatype naming *)
   5.104 @@ -321,8 +281,9 @@
   5.105        val (accs, accs') = pairself (map implode_name) (accesses naming names);
   5.106      in space |> fold (add_name name) accs |> put_accesses name accs' end;
   5.107  
   5.108 -fun declare_binding bnaming (Binding ((prefix, bname), _)) =
   5.109 +fun declare_binding bnaming b =
   5.110    let
   5.111 +    val (prefix, bname) = Binding.dest_binding b;
   5.112      val naming = apply_prefix prefix bnaming;
   5.113      val name = full naming bname;
   5.114    in declare naming name #> pair name end;
   5.115 @@ -343,8 +304,9 @@
   5.116  fun table_declare naming = gen_table_declare Symtab.update_new naming;
   5.117  fun table_declare_permissive naming = gen_table_declare Symtab.update naming;
   5.118  
   5.119 -fun full_binding naming (Binding ((prefix, bname), _)) =
   5.120 -  full (apply_prefix prefix naming) bname;
   5.121 +fun full_binding naming b =
   5.122 +  let val (prefix, bname) = Binding.dest_binding b
   5.123 +  in full (apply_prefix prefix naming) bname end;
   5.124  
   5.125  fun extend_table naming bentries (space, tab) =
   5.126    let val entries = map (apfst (full naming)) bentries
   5.127 @@ -366,6 +328,3 @@
   5.128  val explode = explode_name;
   5.129  
   5.130  end;
   5.131 -
   5.132 -structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
   5.133 -open BasicNameSpace;
     6.1 --- a/src/Pure/Isar/args.ML	Mon Dec 01 16:02:57 2008 +0100
     6.2 +++ b/src/Pure/Isar/args.ML	Mon Dec 01 19:41:16 2008 +0100
     6.3 @@ -171,7 +171,7 @@
     6.4  val name_source_position = named >> T.source_position_of;
     6.5  
     6.6  val name = named >> T.content_of;
     6.7 -val binding = P.position name >> Name.binding_pos;
     6.8 +val binding = P.position name >> Binding.binding_pos;
     6.9  val alt_name = alt_string >> T.content_of;
    6.10  val symbol = symbolic >> T.content_of;
    6.11  val liberal_name = symbol || name;
     7.1 --- a/src/Pure/Isar/class.ML	Mon Dec 01 16:02:57 2008 +0100
     7.2 +++ b/src/Pure/Isar/class.ML	Mon Dec 01 19:41:16 2008 +0100
     7.3 @@ -78,7 +78,7 @@
     7.4  val class_prefix = Logic.const_of_class o Sign.base_name;
     7.5  
     7.6  fun class_name_morphism class =
     7.7 -  Name.map_prefix (K (Name.add_prefix false (class_prefix class)));
     7.8 +  Binding.map_prefix (K (Binding.add_prefix false (class_prefix class)));
     7.9  
    7.10  fun activate_class_morphism thy class inst morphism =
    7.11    Locale.get_interpret_morph thy (class_name_morphism class) (class, "") morphism class inst;
     8.1 --- a/src/Pure/Isar/locale.ML	Mon Dec 01 16:02:57 2008 +0100
     8.2 +++ b/src/Pure/Isar/locale.ML	Mon Dec 01 19:41:16 2008 +0100
     8.3 @@ -947,8 +947,8 @@
     8.4          val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
     8.5          val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
     8.6          val (lprfx, pprfx) = param_prefix name params;
     8.7 -        val add_prefices = pprfx <> "" ? Name.add_prefix false pprfx
     8.8 -          #> Name.add_prefix false lprfx;
     8.9 +        val add_prefices = pprfx <> "" ? Binding.add_prefix false pprfx
    8.10 +          #> Binding.add_prefix false lprfx;
    8.11          val elem_morphism =
    8.12            Element.rename_morphism ren $>
    8.13            Morphism.name_morphism add_prefices $>
    8.14 @@ -1634,10 +1634,10 @@
    8.15  
    8.16  fun name_morph phi_name (lprfx, pprfx) b =
    8.17    b
    8.18 -  |> (if not (Name.is_nothing b) andalso pprfx <> ""
    8.19 -        then Name.add_prefix false pprfx else I)
    8.20 -  |> (if not (Name.is_nothing b)
    8.21 -        then Name.add_prefix false lprfx else I)
    8.22 +  |> (if not (Binding.is_nothing b) andalso pprfx <> ""
    8.23 +        then Binding.add_prefix false pprfx else I)
    8.24 +  |> (if not (Binding.is_nothing b)
    8.25 +        then Binding.add_prefix false lprfx else I)
    8.26    |> phi_name;
    8.27  
    8.28  fun inst_morph thy phi_name param_prfx insts prems eqns export =
    8.29 @@ -2442,11 +2442,11 @@
    8.30    end;
    8.31  
    8.32  fun standard_name_morph interp_prfx b =
    8.33 -  if Name.is_nothing b then b
    8.34 -  else Name.map_prefix (fn ((lprfx, _) :: pprfx) =>
    8.35 -    fold (Name.add_prefix false o fst) pprfx
    8.36 -    #> interp_prfx <> "" ? Name.add_prefix true interp_prfx
    8.37 -    #> Name.add_prefix false lprfx
    8.38 +  if Binding.is_nothing b then b
    8.39 +  else Binding.map_prefix (fn ((lprfx, _) :: pprfx) =>
    8.40 +    fold (Binding.add_prefix false o fst) pprfx
    8.41 +    #> interp_prfx <> "" ? Binding.add_prefix true interp_prfx
    8.42 +    #> Binding.add_prefix false lprfx
    8.43    ) b;
    8.44  
    8.45  in
     9.1 --- a/src/Pure/Isar/outer_parse.ML	Mon Dec 01 16:02:57 2008 +0100
     9.2 +++ b/src/Pure/Isar/outer_parse.ML	Mon Dec 01 19:41:16 2008 +0100
     9.3 @@ -228,7 +228,7 @@
     9.4  (* names and text *)
     9.5  
     9.6  val name = group "name declaration" (short_ident || sym_ident || string || number);
     9.7 -val binding = position name >> Name.binding_pos;
     9.8 +val binding = position name >> Binding.binding_pos;
     9.9  val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
    9.10  val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
    9.11  val path = group "file name/path specification" name >> Path.explode;
    10.1 --- a/src/Pure/Isar/proof_context.ML	Mon Dec 01 16:02:57 2008 +0100
    10.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Dec 01 19:41:16 2008 +0100
    10.3 @@ -971,7 +971,7 @@
    10.4  
    10.5  fun gen_note_thmss get k = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
    10.6    let
    10.7 -    val pos = Name.pos_of b;
    10.8 +    val pos = Binding.pos_of b;
    10.9      val name = full_binding ctxt b;
   10.10      val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos;
   10.11  
   10.12 @@ -1128,7 +1128,7 @@
   10.13        |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
   10.14        |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix);
   10.15      val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
   10.16 -      ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Name.pos_of b));
   10.17 +      ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
   10.18    in (xs', ctxt'') end;
   10.19  
   10.20  in
    11.1 --- a/src/Pure/Isar/specification.ML	Mon Dec 01 16:02:57 2008 +0100
    11.2 +++ b/src/Pure/Isar/specification.ML	Mon Dec 01 19:41:16 2008 +0100
    11.3 @@ -190,7 +190,7 @@
    11.4              val y = Name.name_of b;
    11.5              val _ = x = y orelse
    11.6                error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
    11.7 -                Position.str_of (Name.pos_of b));
    11.8 +                Position.str_of (Binding.pos_of b));
    11.9            in (b, mx) end);
   11.10      val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
   11.11          (var, ((Name.map_name (suffix "_raw") name, []), rhs));
   11.12 @@ -223,7 +223,7 @@
   11.13              val y = Name.name_of b;
   11.14              val _ = x = y orelse
   11.15                error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
   11.16 -                Position.str_of (Name.pos_of b));
   11.17 +                Position.str_of (Binding.pos_of b));
   11.18            in (b, mx) end);
   11.19      val lthy' = lthy
   11.20        |> ProofContext.set_syntax_mode mode    (* FIXME ?!? *)
   11.21 @@ -348,7 +348,7 @@
   11.22          lthy
   11.23          |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
   11.24          |> (fn (res, lthy') =>
   11.25 -          if Name.is_nothing name andalso null atts then
   11.26 +          if Binding.is_nothing name andalso null atts then
   11.27              (ProofDisplay.print_results true lthy' ((kind, ""), res); lthy')
   11.28            else
   11.29              let
    12.1 --- a/src/Pure/Isar/theory_target.ML	Mon Dec 01 16:02:57 2008 +0100
    12.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Dec 01 19:41:16 2008 +0100
    12.3 @@ -201,7 +201,7 @@
    12.4      val arg = (b', Term.close_schematic_term rhs');
    12.5      val similar_body = Type.similar_types (rhs, rhs');
    12.6      (* FIXME workaround based on educated guess *)
    12.7 -    val (prefix', _) = Name.dest_binding b';
    12.8 +    val (prefix', _) = Binding.dest_binding b';
    12.9      val class_global = Name.name_of b = Name.name_of b'
   12.10        andalso not (null prefix')
   12.11        andalso (fst o snd o split_last) prefix' = Class.class_prefix target;
    13.1 --- a/src/Pure/facts.ML	Mon Dec 01 16:02:57 2008 +0100
    13.2 +++ b/src/Pure/facts.ML	Mon Dec 01 19:41:16 2008 +0100
    13.3 @@ -192,7 +192,7 @@
    13.4  
    13.5  fun add permissive do_props naming (b, ths) (Facts {facts, props}) =
    13.6    let
    13.7 -    val (name, facts') = if Name.is_nothing b then ("", facts)
    13.8 +    val (name, facts') = if Binding.is_nothing b then ("", facts)
    13.9        else let
   13.10          val (space, tab) = facts;
   13.11          val (name, space') = NameSpace.declare_binding naming b space;
    14.1 --- a/src/Pure/name.ML	Mon Dec 01 16:02:57 2008 +0100
    14.2 +++ b/src/Pure/name.ML	Mon Dec 01 19:41:16 2008 +0100
    14.3 @@ -29,20 +29,16 @@
    14.4    val variant_list: string list -> string list -> string list
    14.5    val variant: string list -> string -> string
    14.6  
    14.7 -  include NAME_BINDING
    14.8 -  val add_prefix: bool -> string -> binding -> binding
    14.9 -  val map_prefix: ((string * bool) list -> binding -> binding) -> binding -> binding
   14.10 -  val name_of: binding -> string (*FIMXE legacy*)
   14.11 -  val map_name: (string -> string) -> binding -> binding (*FIMXE legacy*)
   14.12 -  val qualified: string -> binding -> binding (*FIMXE legacy*)
   14.13 -  val display: binding -> string
   14.14 +  include BINDING
   14.15 +  type binding = Binding.T
   14.16 +  val name_of: Binding.T -> string (*FIMXE legacy*)
   14.17 +  val map_name: (string -> string) -> Binding.T -> Binding.T (*FIMXE legacy*)
   14.18 +  val qualified: string -> Binding.T -> Binding.T (*FIMXE legacy*)
   14.19  end;
   14.20  
   14.21  structure Name: NAME =
   14.22  struct
   14.23  
   14.24 -open NameSpace;
   14.25 -
   14.26  (** common defaults **)
   14.27  
   14.28  val uu = "uu";
   14.29 @@ -152,27 +148,13 @@
   14.30  
   14.31  (** generic name bindings **)
   14.32  
   14.33 -fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix"
   14.34 -  else (map_binding o apfst) (cons (prfx, sticky)) b;
   14.35 +open Binding;
   14.36 +
   14.37 +type binding = Binding.T;
   14.38  
   14.39  val prefix_of = fst o dest_binding;
   14.40  val name_of = snd o dest_binding;
   14.41  val map_name = map_binding o apsnd;
   14.42  val qualified = map_name o NameSpace.qualified;
   14.43  
   14.44 -fun map_prefix f b =
   14.45 -  let
   14.46 -    val (prefix, name) = dest_binding b;
   14.47 -    val pos = pos_of b;
   14.48 -  in f prefix (binding_pos (name, pos)) end;
   14.49 -
   14.50 -fun display b =
   14.51 -  let
   14.52 -    val (prefix, name) = dest_binding b
   14.53 -    fun mk_prefix (prfx, true) = prfx
   14.54 -      | mk_prefix (prfx, false) = enclose "(" ")" prfx
   14.55 -  in if not (! NameSpace.long_names) orelse null prefix orelse name = "" then name
   14.56 -    else NameSpace.implode (map mk_prefix prefix) ^ ":" ^ name
   14.57 -  end;
   14.58 -
   14.59  end;
    15.1 --- a/src/Pure/pure_thy.ML	Mon Dec 01 16:02:57 2008 +0100
    15.2 +++ b/src/Pure/pure_thy.ML	Mon Dec 01 19:41:16 2008 +0100
    15.3 @@ -144,7 +144,7 @@
    15.4    (FactsData.map (apsnd (fold (cons o lazy_proof) thms)) thy, thms);
    15.5  
    15.6  fun enter_thms pre_name post_name app_att (b, thms) thy =
    15.7 -  if Name.is_nothing b
    15.8 +  if Binding.is_nothing b
    15.9    then swap (enter_proofs (app_att (thy, thms)))
   15.10    else let
   15.11      val naming = Sign.naming_of thy;
   15.12 @@ -198,7 +198,7 @@
   15.13  
   15.14  fun gen_note_thmss tag = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
   15.15    let
   15.16 -    val pos = Name.pos_of b;
   15.17 +    val pos = Binding.pos_of b;
   15.18      val name = Sign.full_binding thy b;
   15.19      val _ = Position.report (Markup.fact_decl name) pos;
   15.20  
    16.1 --- a/src/Pure/sign.ML	Mon Dec 01 16:02:57 2008 +0100
    16.2 +++ b/src/Pure/sign.ML	Mon Dec 01 19:41:16 2008 +0100
    16.3 @@ -535,7 +535,7 @@
    16.4  
    16.5  fun declare_const tags ((b, T), mx) thy =
    16.6    let
    16.7 -    val pos = Name.pos_of b;
    16.8 +    val pos = Binding.pos_of b;
    16.9      val tags' = Position.default_properties pos tags;
   16.10      val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags' [(b, T, mx)] thy;
   16.11      val _ = Position.report (Markup.const_decl c) pos;