src/Pure/sign.ML
changeset 35129 ed24ba6f69aa
parent 34259 2ba492b8b6e8
child 35200 aaddb2b526d6
     1.1 --- a/src/Pure/sign.ML	Mon Feb 15 15:50:41 2010 +0100
     1.2 +++ b/src/Pure/sign.ML	Mon Feb 15 17:17:51 2010 +0100
     1.3 @@ -434,7 +434,7 @@
     1.4  fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
     1.5    let
     1.6      val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Name.of_binding a, n, mx)) types) syn;
     1.7 -    val decls = map (fn (a, n, mx) => (Binding.map_name (Syntax.type_name mx) a, n)) types;
     1.8 +    val decls = map (fn (a, n, _) => (a, n)) types;
     1.9      val tsig' = fold (Type.add_type naming) decls tsig;
    1.10    in (naming, syn', tsig', consts) end);
    1.11  
    1.12 @@ -450,12 +450,11 @@
    1.13  
    1.14  (* add type abbreviations *)
    1.15  
    1.16 -fun gen_add_tyabbr parse_typ (a, vs, rhs, mx) thy =
    1.17 +fun gen_add_tyabbr parse_typ (b, vs, rhs, mx) thy =
    1.18    thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.19      let
    1.20        val ctxt = ProofContext.init thy;
    1.21 -      val syn' = Syntax.update_type_gram [(Name.of_binding a, length vs, mx)] syn;
    1.22 -      val b = Binding.map_name (Syntax.type_name mx) a;
    1.23 +      val syn' = Syntax.update_type_gram [(Name.of_binding b, length vs, mx)] syn;
    1.24        val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
    1.25          handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
    1.26        val tsig' = Type.add_abbrev naming abbr tsig;
    1.27 @@ -471,8 +470,7 @@
    1.28    let
    1.29      val ctxt = ProofContext.init thy;
    1.30      fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
    1.31 -      handle ERROR msg =>
    1.32 -        cat_error msg ("in syntax declaration " ^ quote (Syntax.const_name mx c));
    1.33 +      handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
    1.34    in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
    1.35  
    1.36  fun gen_add_syntax x = gen_syntax Syntax.update_const_gram x;
    1.37 @@ -500,10 +498,8 @@
    1.38    let
    1.39      val ctxt = ProofContext.init thy;
    1.40      val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
    1.41 -    fun prep (raw_b, raw_T, raw_mx) =
    1.42 +    fun prep (b, raw_T, mx) =
    1.43        let
    1.44 -        val (mx_name, mx) = Syntax.const_mixfix (Name.of_binding raw_b) raw_mx;
    1.45 -        val b = Binding.map_name (K mx_name) raw_b;
    1.46          val c = full_name thy b;
    1.47          val c_syn = if authentic then Syntax.constN ^ c else Name.of_binding b;
    1.48          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>