reformatting
authorpaulson
Thu Mar 02 18:51:11 2006 +0100 (2006-03-02)
changeset 1917652b6ecd0433a
parent 19175 c6e4b073f6a5
child 19177 68c6824d8bb6
reformatting
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/res_clause.ML	Thu Mar 02 18:50:43 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Thu Mar 02 18:51:11 2006 +0100
     1.3 @@ -432,7 +432,7 @@
     1.4    | check_var_pairs (x,y) ((u,v)::w) =
     1.5      if (x,y) = (u,v) then 1 
     1.6      else
     1.7 -	if (x = u) orelse (y = v) then 2 (*conflict*)
     1.8 +	if x=u orelse y=v then 2 (*conflict*)
     1.9  	else check_var_pairs (x,y) w;
    1.10  
    1.11  fun type_eq (AtomV(v1),AtomV(v2)) (vars,tvars) =
    1.12 @@ -451,9 +451,7 @@
    1.13        end
    1.14    | type_eq (Comp(_,_),_) vtvars = (false,vtvars)
    1.15  
    1.16 -and
    1.17 -
    1.18 -    types_eq ([],[]) vtvars = (true,vtvars)
    1.19 +and types_eq ([],[]) vtvars = (true,vtvars)
    1.20    | types_eq (tp1::tps1,tp2::tps2) vtvars =
    1.21        let val (eq1,vtvars1) = type_eq (tp1,tp2) vtvars
    1.22  	  val (eq2,vtvars2) = if eq1 then types_eq (tps1,tps2) vtvars1
    1.23 @@ -480,9 +478,7 @@
    1.24        end
    1.25    | term_eq (Fun(_,_,_),_) vtvars = (false,vtvars)
    1.26  
    1.27 -and
    1.28 -
    1.29 -    terms_eq ([],[]) vtvars = (true,vtvars)
    1.30 +and terms_eq ([],[]) vtvars = (true,vtvars)
    1.31    | terms_eq (tm1::tms1,tm2::tms2) vtvars =
    1.32        let val (eq1,vtvars1) = term_eq (tm1,tm2) vtvars
    1.33  	  val (eq2,vtvars2) = if eq1 then terms_eq (tms1,tms2) vtvars1
    1.34 @@ -494,7 +490,7 @@
    1.35  
    1.36  fun pred_eq (Predicate(pname1,tps1,tms1),Predicate(pname2,tps2,tms2)) vtvars =
    1.37      let val (eq1,vtvars1) = 
    1.38 -	    if (pname1 = pname2) then terms_eq (tms1,tms2) vtvars
    1.39 +	    if pname1 = pname2 then terms_eq (tms1,tms2) vtvars
    1.40  	    else (false,vtvars)
    1.41  	val (eq2,vtvars2) = 
    1.42  	    if eq1 then types_eq (tps1,tps2) vtvars1
    1.43 @@ -508,19 +504,18 @@
    1.44      if (pol1 = pol2) then pred_eq (pred1,pred2) vtvars
    1.45      else (false,vtvars);
    1.46  
    1.47 -(*must have the same number of literals*)
    1.48  fun lits_eq ([],[]) vtvars = (true,vtvars)
    1.49    | lits_eq (l1::ls1,l2::ls2) vtvars = 
    1.50 -    let val (eq1,vtvars1) = lit_eq (l1,l2) vtvars
    1.51 -    in
    1.52 -	if eq1 then lits_eq (ls1,ls2) vtvars1
    1.53 -	else (false,vtvars1)
    1.54 -    end;
    1.55 -
    1.56 +      let val (eq1,vtvars1) = lit_eq (l1,l2) vtvars
    1.57 +      in
    1.58 +	  if eq1 then lits_eq (ls1,ls2) vtvars1
    1.59 +	  else (false,vtvars1)
    1.60 +      end
    1.61 +  | lits_eq _ vtvars = (false,vtvars);
    1.62  
    1.63  (*Equality of two clauses up to variable renaming*)
    1.64  fun clause_eq (Clause{literals=lits1,...}, Clause{literals=lits2,...}) =
    1.65 -  length lits1 = length lits2 andalso #1 (lits_eq (lits1,lits2) ([],[]));
    1.66 +  #1 (lits_eq (lits1,lits2) ([],[]));
    1.67  
    1.68  
    1.69  (*** Hash function for clauses ***)