changeset 16983 | c895701d55ea |
parent 16949 | ea65d75e0ce1 |
child 17203 | 29b2563f5c11 |
--- a/src/Pure/drule.ML Mon Aug 01 19:20:36 2005 +0200 +++ b/src/Pure/drule.ML Mon Aug 01 19:20:37 2005 +0200 @@ -379,7 +379,7 @@ fun forall_intr_frees th = let val {prop,thy,...} = rep_thm th in forall_intr_list - (map (cterm_of thy) (sort (make_ord atless) (term_frees prop))) + (map (cterm_of thy) (sort Term.term_ord (term_frees prop))) th end;