src/Pure/sign.ML
changeset 27302 8d12ac6a3e1c
parent 27284 2ddb6a2db65c
child 28017 4919bd124a58
     1.1 --- a/src/Pure/sign.ML	Fri Jun 20 21:00:25 2008 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Jun 20 21:00:26 2008 +0200
     1.3 @@ -439,7 +439,8 @@
     1.4    let
     1.5      val syn' = Syntax.update_type_gram types syn;
     1.6      val decls = map (fn (a, n, mx) => (Syntax.type_name a mx, n)) types;
     1.7 -    val tsig' = Type.add_types naming decls tsig;
     1.8 +    val tags = [(Markup.theory_nameN, Context.theory_name thy)];
     1.9 +    val tsig' = fold (Type.add_type naming tags) decls tsig;
    1.10    in (naming, syn', tsig', consts) end);
    1.11  
    1.12  
    1.13 @@ -448,7 +449,7 @@
    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 ns syn;
    1.17 -    val tsig' = Type.add_nonterminals naming ns tsig;
    1.18 +    val tsig' = fold (Type.add_nonterminal naming []) ns tsig;
    1.19    in (naming, syn', tsig', consts) end);
    1.20  
    1.21  
    1.22 @@ -462,7 +463,7 @@
    1.23        val a' = Syntax.type_name a mx;
    1.24        val abbr = (a', vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
    1.25          handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote a');
    1.26 -      val tsig' = Type.add_abbrevs naming [abbr] tsig;
    1.27 +      val tsig' = Type.add_abbrev naming [] abbr tsig;
    1.28      in (naming, syn', tsig', consts) end);
    1.29  
    1.30  val add_tyabbrs = fold (gen_add_tyabbr Syntax.parse_typ);