1.1 --- a/src/HOL/Tools/res_clause.ML	Wed Dec 14 01:40:43 2005 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Dec 14 06:19:33 2005 +0100
     1.3 @@ -467,8 +467,69 @@
     1.4  val literals_of_term = literals_of_term1 ([],[],[],[]);
     1.5  
     1.6  
     1.7 -fun predicate_ord (Predicate(predname1,_,_),Predicate(predname2,_,_)) = string_ord (predname1,predname2);
     1.8  
     1.9 +fun list_ord _ ([],[]) = EQUAL
    1.10 +  | list_ord _ ([],_) = LESS
    1.11 +  | list_ord _ (_,[]) = GREATER
    1.12 +  | list_ord ord (x::xs, y::ys) =
    1.13 +    let val xy_ord = ord(x,y)
    1.14 +    in
    1.15 +	case xy_ord of EQUAL => list_ord ord (xs,ys)
    1.16 +		     | _ => xy_ord
    1.17 +    end;
    1.18 +
    1.19 +fun type_ord (AtomV(_),AtomV(_)) = EQUAL
    1.20 +  | type_ord (AtomV(_),_) = LESS
    1.21 +  | type_ord (AtomF(_),AtomV(_)) = GREATER
    1.22 +  | type_ord (AtomF(f1),AtomF(f2)) = string_ord (f1,f2)
    1.23 +  | type_ord (AtomF(_),_) = LESS
    1.24 +  | type_ord (Comp(_,_),AtomV(_)) = GREATER
    1.25 +  | type_ord (Comp(_,_),AtomF(_)) = GREATER
    1.26 +  | type_ord (Comp(con1,args1),Comp(con2,args2)) = 
    1.27 +    let val con_ord = string_ord(con1,con2)
    1.28 +    in
    1.29 +	case con_ord of EQUAL => types_ord (args1,args2)
    1.30 +		      | _ => con_ord
    1.31 +    end
    1.32 +and
    1.33 +
    1.34 +types_ord ([],[]) = EQUAL
    1.35 +  | types_ord (tps1,tps2) = list_ord type_ord (tps1,tps2);
    1.36 +
    1.37 +
    1.38 +fun term_ord (UVar(_,_),UVar(_,_)) = EQUAL
    1.39 +  | term_ord (UVar(_,_),_) = LESS
    1.40 +  | term_ord (Fun(_,_,_),UVar(_)) = GREATER
    1.41 +  | term_ord (Fun(f1,tps1,tms1),Fun(f2,tps2,tms2)) = 
    1.42 +    let val fn_ord = string_ord (f1,f2)
    1.43 +    in
    1.44 +	case fn_ord of EQUAL => 
    1.45 +		       let val tms_ord = terms_ord (tms1,tms2)
    1.46 +		       in
    1.47 +			   case tms_ord of EQUAL => types_ord (tps1,tps2)
    1.48 +					 | _ => tms_ord
    1.49 +		       end
    1.50 +		     | _ => fn_ord
    1.51 +    end
    1.52 +
    1.53 +and
    1.54 +
    1.55 +terms_ord ([],[]) = EQUAL
    1.56 +  | terms_ord (tms1,tms2) = list_ord term_ord (tms1,tms2);
    1.57 +
    1.58 +
    1.59 +
    1.60 +fun predicate_ord (Predicate(predname1,ftyps1,ftms1),Predicate(predname2,ftyps2,ftms2)) = 
    1.61 +    let val predname_ord = string_ord (predname1,predname2)
    1.62 +    in
    1.63 +	case predname_ord of EQUAL => 
    1.64 +			     let val ftms_ord = terms_ord(ftms1,ftms2)
    1.65 +			     in
    1.66 +				 case ftms_ord of EQUAL => types_ord(ftyps1,ftyps2)
    1.67 +						| _ => ftms_ord
    1.68 +			     end
    1.69 +			   | _ => predname_ord
    1.70 +    end;
    1.71  
    1.72  fun literal_ord (Literal(false,_,_),Literal(true,_,_)) = LESS
    1.73    | literal_ord (Literal(true,_,_),Literal(false,_,_)) = GREATER