# HG changeset patch
# User nipkow
# Date 780672226 -3600
# Node ID bf9821f58781d0dd7e6a79aa40536874861435c3
# Parent  9d8791da02089dc51f6d49812df0e9d393ea9fab
Modified termord to take account of the Abs-Abs case.

diff -r 9d8791da0208 -r bf9821f58781 src/Pure/thm.ML
--- 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