src/Pure/drule.ML
changeset 4440 9ed4098074bc
parent 4313 03353197410c
child 4588 42bf47c1de1f
     1.1 --- a/src/Pure/drule.ML	Fri Dec 19 09:58:42 1997 +0100
     1.2 +++ b/src/Pure/drule.ML	Fri Dec 19 10:13:47 1997 +0100
     1.3 @@ -215,7 +215,7 @@
     1.4  fun forall_intr_frees th =
     1.5      let val {prop,sign,...} = rep_thm th
     1.6      in  forall_intr_list
     1.7 -         (map (cterm_of sign) (sort atless (term_frees prop)))
     1.8 +         (map (cterm_of sign) (sort (make_ord atless) (term_frees prop)))
     1.9           th
    1.10      end;
    1.11