src/Pure/sign.ML
changeset 30585 6b2ba4666336
parent 30522 e26b80647189
child 31946 99ac0321cd47
     1.1 --- a/src/Pure/sign.ML	Thu Mar 19 13:26:19 2009 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Mar 19 13:28:55 2009 +0100
     1.3 @@ -434,7 +434,7 @@
     1.4  
     1.5  fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
     1.6    let
     1.7 -    val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Binding.name_of a, n, mx)) types) syn;
     1.8 +    val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Name.of_binding a, n, mx)) types) syn;
     1.9      val decls = map (fn (a, n, mx) => (Binding.map_name (Syntax.type_name mx) a, n)) types;
    1.10      val tags = [(Markup.theory_nameN, Context.theory_name thy)];
    1.11      val tsig' = fold (Type.add_type naming tags) decls tsig;
    1.12 @@ -445,7 +445,7 @@
    1.13  
    1.14  fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.15    let
    1.16 -    val syn' = Syntax.update_consts (map Binding.name_of ns) syn;
    1.17 +    val syn' = Syntax.update_consts (map Name.of_binding ns) syn;
    1.18      val tsig' = fold (Type.add_nonterminal naming []) ns tsig;
    1.19    in (naming, syn', tsig', consts) end);
    1.20  
    1.21 @@ -456,7 +456,7 @@
    1.22    thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.23      let
    1.24        val ctxt = ProofContext.init thy;
    1.25 -      val syn' = Syntax.update_type_gram [(Binding.name_of a, length vs, mx)] syn;
    1.26 +      val syn' = Syntax.update_type_gram [(Name.of_binding a, length vs, mx)] syn;
    1.27        val b = Binding.map_name (Syntax.type_name mx) a;
    1.28        val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
    1.29          handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
    1.30 @@ -504,10 +504,10 @@
    1.31      val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
    1.32      fun prep (raw_b, raw_T, raw_mx) =
    1.33        let
    1.34 -        val (mx_name, mx) = Syntax.const_mixfix (Binding.name_of raw_b) raw_mx;
    1.35 +        val (mx_name, mx) = Syntax.const_mixfix (Name.of_binding raw_b) raw_mx;
    1.36          val b = Binding.map_name (K mx_name) raw_b;
    1.37          val c = full_name thy b;
    1.38 -        val c_syn = if authentic then Syntax.constN ^ c else Binding.name_of b;
    1.39 +        val c_syn = if authentic then Syntax.constN ^ c else Name.of_binding b;
    1.40          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
    1.41            cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
    1.42          val T' = Logic.varifyT T;
    1.43 @@ -568,7 +568,7 @@
    1.44  fun primitive_class (bclass, classes) thy =
    1.45    thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.46      let
    1.47 -      val syn' = Syntax.update_consts [Binding.name_of bclass] syn;
    1.48 +      val syn' = Syntax.update_consts [Name.of_binding bclass] syn;
    1.49        val tsig' = Type.add_class (Syntax.pp_global thy) naming (bclass, classes) tsig;
    1.50      in (naming, syn', tsig', consts) end)
    1.51    |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];