# HG changeset patch
# User wenzelm
# Date 882522951 -3600
# Node ID d55e85d7f0c21214bc3bb77e0acc3bd7df5db99a
# Parent  8ed9e689a15e00da6cabd1b14382ec9a1c06e4eb
term order stuff moved to term.ML;

diff -r 8ed9e689a15e -r d55e85d7f0c2 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Fri Dec 19 10:15:26 1997 +0100
+++ b/src/Pure/logic.ML	Fri Dec 19 10:15:51 1997 +0100
@@ -10,12 +10,6 @@
 
 signature LOGIC = 
 sig
-  val indexname_ord	: indexname * indexname -> order
-  val typ_ord		: typ * typ -> order
-  val typs_ord		: typ list * typ list -> order
-  val term_ord		: term * term -> order
-  val terms_ord		: term list * term list -> order
-  val termless		: term * term -> bool
   val assum_pairs	: term -> (term*term)list
   val auto_rename	: bool ref   
   val close_form	: term -> term   
@@ -60,58 +54,6 @@
 struct
 
 
-(** type and term orders **)
-
-fun indexname_ord ((x, i), (y, j)) =
-  (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
-
-
-(* typ_ord *)
-
-(*assumes that TFrees / TVars with the same name have same sorts*)
-fun typ_ord (Type (a, Ts), Type (b, Us)) =
-      (case string_ord (a, b) of EQUAL => typs_ord (Ts, Us) | ord => ord)
-  | typ_ord (Type _, _) = GREATER
-  | typ_ord (TFree _, Type _) = LESS
-  | typ_ord (TFree (a, _), TFree (b, _)) = string_ord (a, b)
-  | typ_ord (TFree _, TVar _) = GREATER
-  | typ_ord (TVar _, Type _) = LESS
-  | typ_ord (TVar _, TFree _) = LESS
-  | typ_ord (TVar (xi, _), TVar (yj, _)) = indexname_ord (xi, yj)
-and typs_ord Ts_Us = list_ord typ_ord Ts_Us;
-
-
-(* term_ord *)
-
-(*a linear well-founded AC-compatible ordering for terms:
-  s < t <=> 1. size(s) < size(t) or
-            2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
-            3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
-               (s1..sn) < (t1..tn) (lexicographically)*)
-
-fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
-  | dest_hd (Free (a, T)) = (((a, 0), T), 1)
-  | dest_hd (Var v) = (v, 2)
-  | dest_hd (Bound i) = ((("", i), dummyT), 3)
-  | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
-
-fun term_ord (Abs (_, T, t), Abs(_, U, u)) =
-      (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
-  | term_ord (t, u) =
-      (case int_ord (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 hd_ord (f, g) of EQUAL => terms_ord (ts, us) | ord => ord)
-          end
-      | ord => ord)
-and hd_ord (f, g) =
-  prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
-and terms_ord (ts, us) = list_ord term_ord (ts, us);
-
-fun termless tu = (term_ord tu = LESS);
-
-
-
 (*** Abstract syntax operations on the meta-connectives ***)
 
 (** equality **)
@@ -227,8 +169,7 @@
 
 (*Close up a formula over all free variables by quantification*)
 fun close_form A =
-    list_all_free (map dest_Free (sort atless (term_frees A)),   
-		   A);
+  list_all_free (sort_wrt fst (map dest_Free (term_frees A)), A);
 
 
 (*** Specialized operations for resolution... ***)