src/Pure/sign.ML
changeset 42287 d98eb048a2e4
parent 42284 326f57825e1a
child 42288 2074b31650e6
     1.1 --- a/src/Pure/sign.ML	Fri Apr 08 14:05:31 2011 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Apr 08 14:20:57 2011 +0200
     1.3 @@ -334,7 +334,7 @@
     1.4  fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
     1.5    let
     1.6      fun type_syntax (b, n, mx) =
     1.7 -      (Syntax.mark_type (Name_Space.full_name naming b), Syntax.make_type n, mx);
     1.8 +      (Syntax.mark_type (Name_Space.full_name naming b), Mixfix.make_type n, mx);
     1.9      val syn' = Syntax.update_type_gram true Syntax.mode_default (map type_syntax types) syn;
    1.10      val tsig' = fold (fn (a, n, _) => Type.add_type naming (a, n)) types tsig;
    1.11    in (naming, syn', tsig', consts) end);
    1.12 @@ -373,7 +373,7 @@
    1.13  fun type_notation add mode args =
    1.14    let
    1.15      fun type_syntax (Type (c, args), mx) =
    1.16 -          SOME (Syntax.mark_type c, Syntax.make_type (length args), mx)
    1.17 +          SOME (Syntax.mark_type c, Mixfix.make_type (length args), mx)
    1.18        | type_syntax _ = NONE;
    1.19    in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end;
    1.20