src/Pure/drule.ML

--- a/src/Pure/drule.ML	Fri Dec 19 09:58:42 1997 +0100
+++ b/src/Pure/drule.ML	Fri Dec 19 10:13:47 1997 +0100
@@ -215,7 +215,7 @@
 fun forall_intr_frees th =
     let val {prop,sign,...} = rep_thm th
     in  forall_intr_list
-         (map (cterm_of sign) (sort atless (term_frees prop)))
+         (map (cterm_of sign) (sort (make_ord atless) (term_frees prop)))
          th
     end;