Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/axclass.ML
changeset 31904 a86896359ca4
parent 31249 d51d2a22a4f9
child 31943 5e960a0780a2 
--- a/src/Pure/axclass.ML	Thu Jul 02 20:55:44 2009 +0200
+++ b/src/Pure/axclass.ML	Thu Jul 02 21:26:18 2009 +0200
@@ -580,7 +580,7 @@
               | T as TVar (_, S) => insert (eq_fst op =) (T, S)
               | _ => I) typ [];
         val hyps = vars
-          |> map (fn (T, S) => (T, Drule.sort_triv thy (T, S) ~~ S));
+          |> map (fn (T, S) => (T, Thm.sort_triv thy (T, S) ~~ S));
         val ths = (typ, sort)
           |> Sorts.of_sort_derivation (Syntax.pp_global thy) (Sign.classes_of thy)
            {class_relation =
isabelle