src/Pure/sign.ML
changeset 42387 b1965c8992c8
parent 42383 0ae4ad40d7b5
child 42388 a44b0fdaa6c2
     1.1 --- a/src/Pure/sign.ML	Mon Apr 18 12:11:58 2011 +0200
     1.2 +++ b/src/Pure/sign.ML	Mon Apr 18 13:26:39 2011 +0200
     1.3 @@ -144,12 +144,13 @@
     1.4  
     1.5    fun merge pp (sign1, sign2) =
     1.6      let
     1.7 +      val ctxt = Syntax.init_pretty pp;
     1.8        val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1;
     1.9        val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
    1.10  
    1.11        val naming = Name_Space.default_naming;
    1.12        val syn = Syntax.merge_syntaxes syn1 syn2;
    1.13 -      val tsig = Type.merge_tsig pp (tsig1, tsig2);
    1.14 +      val tsig = Type.merge_tsig ctxt (tsig1, tsig2);
    1.15        val consts = Consts.merge (consts1, consts2);
    1.16      in make_sign (naming, syn, tsig, consts) end;
    1.17  );
    1.18 @@ -455,15 +456,19 @@
    1.19  (* primitive classes and arities *)
    1.20  
    1.21  fun primitive_class (bclass, classes) thy =
    1.22 -  thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.23 +  thy
    1.24 +  |> map_sign (fn (naming, syn, tsig, consts) =>
    1.25      let
    1.26        val ctxt = Syntax.init_pretty_global thy;
    1.27 -      val tsig' = Type.add_class ctxt (Context.pretty ctxt) naming (bclass, classes) tsig;
    1.28 +      val tsig' = Type.add_class ctxt naming (bclass, classes) tsig;
    1.29      in (naming, syn, tsig', consts) end)
    1.30    |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
    1.31  
    1.32 -fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Context.pretty_global thy) arg);
    1.33 -fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (Context.pretty_global thy) arg);
    1.34 +fun primitive_classrel arg thy =
    1.35 +  thy |> map_tsig (Type.add_classrel (Syntax.init_pretty_global thy) arg);
    1.36 +
    1.37 +fun primitive_arity arg thy =
    1.38 +  thy |> map_tsig (Type.add_arity (Syntax.init_pretty_global thy) arg);
    1.39  
    1.40  
    1.41  (* add translation functions *)