src/Pure/Isar/expression.ML

 
 signature EXPRESSION =
 sig
   datatype 'term map = Positional of 'term option list | Named of (string * 'term) list;
   type 'term expr = (string * (string * 'term map)) list;
-  type expression = string expr * (Name.binding * string option * mixfix) list;
-  type expression_i = term expr * (Name.binding * typ option * mixfix) list;
+  type expression = string expr * (Binding.T * string option * mixfix) list;
+  type expression_i = term expr * (Binding.T * typ option * mixfix) list;
 
   (* Processing of context statements *)
   val read_statement: Element.context list -> (string * string list) list list ->
     Proof.context ->  (term * term list) list list * Proof.context;
   val cert_statement: Element.context_i list -> (term * term list) list list ->

   Positional of 'term option list |
   Named of (string * 'term) list;
 
 type 'term expr = (string * (string * 'term map)) list;
 
-type expression = string expr * (Name.binding * string option * mixfix) list;
-type expression_i = term expr * (Name.binding * typ option * mixfix) list;
+type expression = string expr * (Binding.T * string option * mixfix) list;
+type expression_i = term expr * (Binding.T * typ option * mixfix) list;
 
 
 (** Parsing and printing **)
 
 local

                 val (ps', i') = params_inst i;
                 val ps'' = AList.join bind_eq (fn p => fn (mx1, mx2) =>
                   (* FIXME: should check for bindings being the same.
                      Instead we check for equal name and syntax. *)
                   if mx1 = mx2 then mx1
-                  else error ("Conflicting syntax for parameter" ^ quote (Name.display p) ^
+                  else error ("Conflicting syntax for parameter" ^ quote (Binding.display p) ^
                     " in expression.")) (ps, ps')
               in (i', ps'') end) is []
           in (ps', is') end;
 
     val (implicit, expr') = params_expr expr;

         inst => SOME inst);
     val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
     val inst = Symtab.make insts'';
   in
     (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
-      Morphism.name_morphism (Name.qualified prfx), ctxt')
+      Morphism.binding_morphism (Binding.qualify prfx), ctxt')
   end;
 
 
 (*** Locale processing ***)
 
 (** Parsing **)
 
 fun parse_elem prep_typ prep_term ctxt elem =
-  Element.map_ctxt {name = I, var = I, typ = prep_typ ctxt,
+  Element.map_ctxt {binding = I, var = I, typ = prep_typ ctxt,
     term = prep_term ctxt, fact = I, attrib = I} elem;
 
 fun parse_concl prep_term ctxt concl =
   (map o map) (fn (t, ps) =>
     (prep_term ctxt, map (prep_term ctxt) ps)) concl;

 
 fun declare_elem prep_vars (Fixes fixes) ctxt =
       let val (vars, _) = prep_vars fixes ctxt
       in ctxt |> ProofContext.add_fixes_i vars |> snd end
   | declare_elem prep_vars (Constrains csts) ctxt =
-      ctxt |> prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) |> snd
+      ctxt |> prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) |> snd
   | declare_elem _ (Assumes _) ctxt = ctxt
   | declare_elem _ (Defines _) ctxt = ctxt
   | declare_elem _ (Notes _) ctxt = ctxt;
 
 (** Finish locale elements, extract specification text **)

     val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
     val asm' = Option.map (Morphism.term morph) asm;
     val defs' = map (Morphism.term morph) defs;
     val text' = text |>
       (if is_some asm
-        then eval_text ctxt false (Assumes [(Attrib.no_binding, [(the asm', [])])])
+        then eval_text ctxt false (Assumes [(Attrib.empty_binding, [(the asm', [])])])
         else I) |>
       (if not (null defs)
-        then eval_text ctxt false (Defines (map (fn def => (Attrib.no_binding, (def, []))) defs'))
+        then eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs'))
         else I)
 (* FIXME clone from new_locale.ML *)
   in ((loc, morph), text') end;
 
 fun finish_elem ctxt parms do_close elem text =

     val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
 (*    val exp_term = TermSubst.zero_var_indexes o Morphism.term export; *)
     val exp_term = Drule.term_rule thy (singleton exp_fact);
     val exp_typ = Logic.type_map exp_term;
     val export' =
-      Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
+      Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
   in ((propss, deps, export'), goal_ctxt) end;
     
 in
 
 fun read_goal_expression x = prep_goal_expression read_full_context_statement x;

    - thy: the theory
 *)
 
 fun def_pred bname parms defs ts norm_ts thy =
   let
-    val name = Sign.full_name thy bname;
+    val name = Sign.full_bname thy bname;
 
     val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
     val env = Term.add_term_free_names (body, []);
     val xs = filter (member (op =) env o #1) parms;
     val Ts = map #2 xs;

     val statement = ObjectLogic.ensure_propT thy head;
 
     val ([pred_def], defs_thy) =
       thy
       |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
-      |> Sign.declare_const [] ((Name.binding bname, predT), NoSyn) |> snd
+      |> Sign.declare_const [] ((Binding.name bname, predT), NoSyn) |> snd
       |> PureThy.add_defs false
         [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
     val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
 
     val cert = Thm.cterm_of defs_thy;

           val (_, thy'') =
             thy'
             |> Sign.add_path aname
             |> Sign.no_base_names
             |> PureThy.note_thmss Thm.internalK
-              [((Name.binding introN, []), [([intro], [NewLocale.unfold_attrib])])]
+              [((Binding.name introN, []), [([intro], [NewLocale.unfold_attrib])])]
             ||> Sign.restore_naming thy';
           in (SOME statement, SOME intro, axioms, thy'') end;
     val (b_pred, b_intro, b_axioms, thy'''') =
       if null ints then (NONE, NONE, [], thy'')
       else

           val (_, thy'''') =
             thy'''
             |> Sign.add_path pname
             |> Sign.no_base_names
             |> PureThy.note_thmss Thm.internalK
-                 [((Name.binding introN, []), [([intro], [NewLocale.intro_attrib])]),
-                  ((Name.binding axiomsN, []),
+                 [((Binding.name introN, []), [([intro], [NewLocale.intro_attrib])]),
+                  ((Binding.name axiomsN, []),
                     [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
             ||> Sign.restore_naming thy''';
         in (SOME statement, SOME intro, axioms, thy'''') end;
   in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy'''') end;
 

 
 fun gen_add_locale prep_decl
     bname predicate_name raw_imprt raw_body thy =
   let
     val thy_ctxt = ProofContext.init thy;
-    val name = Sign.full_name thy bname;
+    val name = Sign.full_bname thy bname;
     val _ = NewLocale.test_locale thy name andalso
       error ("Duplicate definition of locale " ^ quote name);
 
     val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), defs)) =
       prep_decl raw_imprt raw_body thy_ctxt;

     val notes = body_elems' |>
       (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
       fst |> map (Element.morph_ctxt satisfy) |>
       map_filter (fn Notes notes => SOME notes | _ => NONE) |>
       (if is_some asm
-        then cons (Thm.internalK, [((Name.binding (bname ^ "_" ^ axiomsN), []),
+        then cons (Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []),
           [([assume (cterm_of thy' (the asm))], [(Attrib.internal o K) NewLocale.witness_attrib])])])
         else I);
 
     val deps' = map (fn (l, morph) => (l, morph $> satisfy)) deps;