src/Pure/drule.ML
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;