src/Pure/axclass.ML
changeset 31904 a86896359ca4
parent 31249 d51d2a22a4f9
child 31943 5e960a0780a2
     1.1 --- a/src/Pure/axclass.ML	Thu Jul 02 20:55:44 2009 +0200
     1.2 +++ b/src/Pure/axclass.ML	Thu Jul 02 21:26:18 2009 +0200
     1.3 @@ -580,7 +580,7 @@
     1.4                | T as TVar (_, S) => insert (eq_fst op =) (T, S)
     1.5                | _ => I) typ [];
     1.6          val hyps = vars
     1.7 -          |> map (fn (T, S) => (T, Drule.sort_triv thy (T, S) ~~ S));
     1.8 +          |> map (fn (T, S) => (T, Thm.sort_triv thy (T, S) ~~ S));
     1.9          val ths = (typ, sort)
    1.10            |> Sorts.of_sort_derivation (Syntax.pp_global thy) (Sign.classes_of thy)
    1.11             {class_relation =