Modified termord to take account of the Abs-Abs case.

--- a/src/Pure/thm.ML	Mon Sep 26 17:56:21 1994 +0100
+++ b/src/Pure/thm.ML	Tue Sep 27 14:23:46 1994 +0100
@@ -1137,7 +1137,8 @@
 
 (* FIXME: should really take types into account as well.
  * Otherwise non-linear *)
-fun termord(t,u) =
+fun termord(Abs(_,_,t),Abs(_,_,u)) = termord(t,u)
+  | termord(t,u) =
       (case intord(size_of_term t,size_of_term u) of
          EQUAL => let val (f,ts) = strip_comb t and (g,us) = strip_comb u
                   in case stringord(string_of_hd f, string_of_hd g) of