# HG changeset patch
# User paulson
# Date 1141321871 -3600
# Node ID 52b6ecd0433a01e8433bfe962692fe97295fb2a1
# Parent  c6e4b073f6a5aeb0debca24597c9af8eab9fbde8
reformatting

diff -r c6e4b073f6a5 -r 52b6ecd0433a src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Thu Mar 02 18:50:43 2006 +0100
+++ b/src/HOL/Tools/res_clause.ML	Thu Mar 02 18:51:11 2006 +0100
@@ -432,7 +432,7 @@
   | check_var_pairs (x,y) ((u,v)::w) =
     if (x,y) = (u,v) then 1 
     else
-	if (x = u) orelse (y = v) then 2 (*conflict*)
+	if x=u orelse y=v then 2 (*conflict*)
 	else check_var_pairs (x,y) w;
 
 fun type_eq (AtomV(v1),AtomV(v2)) (vars,tvars) =
@@ -451,9 +451,7 @@
       end
   | type_eq (Comp(_,_),_) vtvars = (false,vtvars)
 
-and
-
-    types_eq ([],[]) vtvars = (true,vtvars)
+and types_eq ([],[]) vtvars = (true,vtvars)
   | types_eq (tp1::tps1,tp2::tps2) vtvars =
       let val (eq1,vtvars1) = type_eq (tp1,tp2) vtvars
 	  val (eq2,vtvars2) = if eq1 then types_eq (tps1,tps2) vtvars1
@@ -480,9 +478,7 @@
       end
   | term_eq (Fun(_,_,_),_) vtvars = (false,vtvars)
 
-and
-
-    terms_eq ([],[]) vtvars = (true,vtvars)
+and terms_eq ([],[]) vtvars = (true,vtvars)
   | terms_eq (tm1::tms1,tm2::tms2) vtvars =
       let val (eq1,vtvars1) = term_eq (tm1,tm2) vtvars
 	  val (eq2,vtvars2) = if eq1 then terms_eq (tms1,tms2) vtvars1
@@ -494,7 +490,7 @@
 
 fun pred_eq (Predicate(pname1,tps1,tms1),Predicate(pname2,tps2,tms2)) vtvars =
     let val (eq1,vtvars1) = 
-	    if (pname1 = pname2) then terms_eq (tms1,tms2) vtvars
+	    if pname1 = pname2 then terms_eq (tms1,tms2) vtvars
 	    else (false,vtvars)
 	val (eq2,vtvars2) = 
 	    if eq1 then types_eq (tps1,tps2) vtvars1
@@ -508,19 +504,18 @@
     if (pol1 = pol2) then pred_eq (pred1,pred2) vtvars
     else (false,vtvars);
 
-(*must have the same number of literals*)
 fun lits_eq ([],[]) vtvars = (true,vtvars)
   | lits_eq (l1::ls1,l2::ls2) vtvars = 
-    let val (eq1,vtvars1) = lit_eq (l1,l2) vtvars
-    in
-	if eq1 then lits_eq (ls1,ls2) vtvars1
-	else (false,vtvars1)
-    end;
-
+      let val (eq1,vtvars1) = lit_eq (l1,l2) vtvars
+      in
+	  if eq1 then lits_eq (ls1,ls2) vtvars1
+	  else (false,vtvars1)
+      end
+  | lits_eq _ vtvars = (false,vtvars);
 
 (*Equality of two clauses up to variable renaming*)
 fun clause_eq (Clause{literals=lits1,...}, Clause{literals=lits2,...}) =
-  length lits1 = length lits2 andalso #1 (lits_eq (lits1,lits2) ([],[]));
+  #1 (lits_eq (lits1,lits2) ([],[]));
 
 
 (*** Hash function for clauses ***)