src/Pure/axclass.ML
changeset 22570 f166a5416b3f
parent 22385 cc2be3315e72
child 22691 290454649b8c
     1.1 --- a/src/Pure/axclass.ML	Tue Apr 03 19:24:15 2007 +0200
     1.2 +++ b/src/Pure/axclass.ML	Tue Apr 03 19:24:16 2007 +0200
     1.3 @@ -436,13 +436,13 @@
     1.4          val hyps = vars
     1.5            |> map (fn (T, S) => (T, Drule.sort_triv thy (T, S) ~~ S));
     1.6          val ths = (typ, sort) |> Sorts.of_sort_derivation (Sign.pp thy) (Sign.classes_of thy)
     1.7 -           {classrel =
     1.8 +           {class_relation =
     1.9                fn (th, c1) => fn c2 => th RS the_classrel thy (c1, c2),
    1.10 -            constructor =
    1.11 +            type_constructor =
    1.12                fn a => fn dom => fn c =>
    1.13                  let val Ss = map (map snd) dom and ths = maps (map fst) dom
    1.14                  in ths MRS the_arity thy a (c, Ss) end,
    1.15 -            variable =
    1.16 +            type_variable =
    1.17                the_default [] o AList.lookup (op =) hyps};
    1.18        in ths end;
    1.19