Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
authorpaulson
Wed Jan 17 09:52:06 2007 +0100 (2007-01-17)
changeset 220785084f53cef39
parent 22077 2882d9cc5e75
child 22079 b161604f0c8d
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
minimize_applies is now by default TRUE!
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Tue Jan 16 14:11:25 2007 +0100
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Wed Jan 17 09:52:06 2007 +0100
     1.3 @@ -8,6 +8,8 @@
     1.4  
     1.5  struct
     1.6  
     1.7 +structure RC = ResClause;
     1.8 +
     1.9  (* theorems for combinators and function extensionality *)
    1.10  val ext = thm "HOL.ext";
    1.11  val comb_I = thm "ATP_Linkup.COMBI_def";
    1.12 @@ -27,7 +29,7 @@
    1.13  
    1.14  (*If true, each function will be directly applied to as many arguments as possible, avoiding
    1.15    use of the "apply" operator. Use of hBOOL is also minimized.*)
    1.16 -val minimize_applies = ref false;
    1.17 +val minimize_applies = ref true;
    1.18  
    1.19  val const_typargs = ref (Library.K [] : (string*typ -> typ list));
    1.20  
    1.21 @@ -132,7 +134,7 @@
    1.22  		val tS = [tp',tq',t1] ---> tpq
    1.23  	    in  compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ Q') bnds  end
    1.24        end
    1.25 -  | lam2comb (t as (Abs(x,t1,_))) _ = raise ResClause.CLAUSE("HOL CLAUSE",t);
    1.26 +  | lam2comb (t as (Abs(x,t1,_))) _ = raise RC.CLAUSE("HOL CLAUSE",t);
    1.27  
    1.28  fun to_comb (Abs(x,tp,b)) bnds = lam2comb (Abs(x, tp, to_comb b (tp::bnds))) bnds 
    1.29    | to_comb (P $ Q) bnds = (to_comb P bnds) $ (to_comb Q bnds)
    1.30 @@ -158,10 +160,10 @@
    1.31  type polarity = bool;
    1.32  type clause_id = int;
    1.33  
    1.34 -datatype combterm = CombConst of string * ResClause.fol_type * ResClause.fol_type list
    1.35 -		  | CombFree of string * ResClause.fol_type
    1.36 -		  | CombVar of string * ResClause.fol_type
    1.37 -		  | CombApp of combterm * combterm * ResClause.fol_type
    1.38 +datatype combterm = CombConst of string * RC.fol_type * RC.fol_type list
    1.39 +		  | CombFree of string * RC.fol_type
    1.40 +		  | CombVar of string * RC.fol_type
    1.41 +		  | CombApp of combterm * combterm
    1.42  		  
    1.43  datatype literal = Literal of polarity * combterm;
    1.44  
    1.45 @@ -169,11 +171,11 @@
    1.46  	 Clause of {clause_id: clause_id,
    1.47  		    axiom_name: axiom_name,
    1.48  		    th: thm,
    1.49 -		    kind: ResClause.kind,
    1.50 +		    kind: RC.kind,
    1.51  		    literals: literal list,
    1.52 -		    ctypes_sorts: (ResClause.typ_var * Term.sort) list, 
    1.53 -                    ctvar_type_literals: ResClause.type_literal list, 
    1.54 -                    ctfree_type_literals: ResClause.type_literal list};
    1.55 +		    ctypes_sorts: (RC.typ_var * Term.sort) list, 
    1.56 +                    ctvar_type_literals: RC.type_literal list, 
    1.57 +                    ctfree_type_literals: RC.type_literal list};
    1.58  
    1.59  
    1.60  (*********************************************************************)
    1.61 @@ -194,73 +196,44 @@
    1.62  
    1.63  fun type_of (Type (a, Ts)) =
    1.64        let val (folTypes,ts) = types_of Ts
    1.65 -	  val t = ResClause.make_fixed_type_const a
    1.66 -      in
    1.67 -	  (ResClause.mk_fol_type("Comp",t,folTypes), ts)
    1.68 -      end
    1.69 +      in  (RC.Comp(RC.make_fixed_type_const a, folTypes), ts)  end
    1.70    | type_of (tp as (TFree(a,s))) =
    1.71 -      let val t = ResClause.make_fixed_type_var a
    1.72 -      in
    1.73 -	  (ResClause.mk_fol_type("Fixed",t,[]), [ResClause.mk_typ_var_sort tp])
    1.74 -      end
    1.75 +      (RC.AtomF (RC.make_fixed_type_var a), [RC.mk_typ_var_sort tp])
    1.76    | type_of (tp as (TVar(v,s))) =
    1.77 -      let val t = ResClause.make_schematic_type_var v
    1.78 -      in
    1.79 -	  (ResClause.mk_fol_type("Var",t,[]), [ResClause.mk_typ_var_sort tp])
    1.80 -      end
    1.81 +      (RC.AtomV (RC.make_schematic_type_var v), [RC.mk_typ_var_sort tp])
    1.82  and types_of Ts =
    1.83 -      let val foltyps_ts = map type_of Ts
    1.84 -	  val (folTyps,ts) = ListPair.unzip foltyps_ts
    1.85 -      in
    1.86 -	  (folTyps, ResClause.union_all ts)
    1.87 -      end;
    1.88 +      let val (folTyps,ts) = ListPair.unzip (map type_of Ts)
    1.89 +      in  (folTyps, RC.union_all ts)  end;
    1.90  
    1.91  (* same as above, but no gathering of sort information *)
    1.92  fun simp_type_of (Type (a, Ts)) = 
    1.93 -      let val typs = map simp_type_of Ts
    1.94 -	  val t = ResClause.make_fixed_type_const a
    1.95 -      in
    1.96 -	  ResClause.mk_fol_type("Comp",t,typs)
    1.97 -      end
    1.98 -  | simp_type_of (TFree (a,s)) = ResClause.mk_fol_type("Fixed",ResClause.make_fixed_type_var a,[])
    1.99 -  | simp_type_of (TVar (v,s)) = ResClause.mk_fol_type("Var",ResClause.make_schematic_type_var v,[]);
   1.100 +      RC.Comp(RC.make_fixed_type_const a, map simp_type_of Ts)
   1.101 +  | simp_type_of (TFree (a,s)) = RC.AtomF(RC.make_fixed_type_var a)
   1.102 +  | simp_type_of (TVar (v,s)) = RC.AtomV(RC.make_schematic_type_var v);
   1.103  
   1.104  
   1.105  fun const_type_of (c,t) =
   1.106 -    let val (tp,ts) = type_of t
   1.107 -	val tvars = !const_typargs(c,t)
   1.108 -    in
   1.109 -	(tp, ts, map simp_type_of tvars)
   1.110 -    end;
   1.111 +      let val (tp,ts) = type_of t
   1.112 +      in  (tp, ts, map simp_type_of (!const_typargs(c,t))) end;
   1.113  
   1.114  (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
   1.115  fun combterm_of (Const(c,t)) =
   1.116        let val (tp,ts,tvar_list) = const_type_of (c,t)
   1.117 -	  val c' = CombConst(ResClause.make_fixed_const c,tp,tvar_list)
   1.118 -      in
   1.119 -	  (c',ts)
   1.120 -      end
   1.121 +	  val c' = CombConst(RC.make_fixed_const c, tp, tvar_list)
   1.122 +      in  (c',ts)  end
   1.123    | combterm_of (Free(v,t)) =
   1.124        let val (tp,ts) = type_of t
   1.125 -	  val v' = if ResClause.isMeta v then CombVar(ResClause.make_schematic_var(v,0),tp)
   1.126 -		   else CombFree(ResClause.make_fixed_var v,tp)
   1.127 -      in
   1.128 -	  (v',ts)
   1.129 -      end
   1.130 +	  val v' = if RC.isMeta v then CombVar(RC.make_schematic_var(v,0),tp)
   1.131 +		   else CombFree(RC.make_fixed_var v,tp)
   1.132 +      in  (v',ts)  end
   1.133    | combterm_of (Var(v,t)) =
   1.134        let val (tp,ts) = type_of t
   1.135 -	  val v' = CombVar(ResClause.make_schematic_var v,tp)
   1.136 -      in
   1.137 -	  (v',ts)
   1.138 -      end
   1.139 +	  val v' = CombVar(RC.make_schematic_var v,tp)
   1.140 +      in  (v',ts)  end
   1.141    | combterm_of (t as (P $ Q)) =
   1.142        let val (P',tsP) = combterm_of P
   1.143  	  val (Q',tsQ) = combterm_of Q
   1.144 -	  val tp = Term.type_of t
   1.145 -	  val t' = CombApp(P',Q', simp_type_of tp)
   1.146 -      in
   1.147 -	  (t',tsP union tsQ)
   1.148 -      end;
   1.149 +      in  (CombApp(P',Q'), tsP union tsQ)  end;
   1.150  
   1.151  fun predicate_of ((Const("Not",_) $ P), polarity) = predicate_of (P, not polarity)
   1.152    | predicate_of (t,polarity) = (combterm_of t, polarity);
   1.153 @@ -279,7 +252,7 @@
   1.154  (* making axiom and conjecture clauses *)
   1.155  fun make_clause(clause_id,axiom_name,kind,th) =
   1.156      let val (lits,ctypes_sorts) = literals_of_term (to_comb (prop_of th) [])
   1.157 -	val (ctvar_lits,ctfree_lits) = ResClause.add_typs_aux ctypes_sorts
   1.158 +	val (ctvar_lits,ctfree_lits) = RC.add_typs_aux ctypes_sorts
   1.159      in
   1.160  	if forall isFalse lits
   1.161  	then error "Problem too trivial for resolution (empty clause)"
   1.162 @@ -292,7 +265,7 @@
   1.163  
   1.164  
   1.165  fun add_axiom_clause ((th,(name,id)), pairs) =
   1.166 -  let val cls = make_clause(id, name, ResClause.Axiom, th)
   1.167 +  let val cls = make_clause(id, name, RC.Axiom, th)
   1.168    in
   1.169        if isTaut cls then pairs else (name,cls)::pairs
   1.170    end;
   1.171 @@ -301,7 +274,7 @@
   1.172  
   1.173  fun make_conjecture_clauses_aux _ [] = []
   1.174    | make_conjecture_clauses_aux n (th::ths) =
   1.175 -      make_clause(n,"conjecture", ResClause.Conjecture, th) ::
   1.176 +      make_clause(n,"conjecture", RC.Conjecture, th) ::
   1.177        make_conjecture_clauses_aux (n+1) ths;
   1.178  
   1.179  val make_conjecture_clauses = make_conjecture_clauses_aux 0;
   1.180 @@ -316,22 +289,26 @@
   1.181  val type_wrapper = "typeinfo";
   1.182  
   1.183  fun wrap_type (c,tp) = case !typ_level of
   1.184 -	T_FULL => type_wrapper ^ ResClause.paren_pack [c, ResClause.string_of_fol_type tp]
   1.185 +	T_FULL => type_wrapper ^ RC.paren_pack [c, RC.string_of_fol_type tp]
   1.186        | _ => c;
   1.187      
   1.188  
   1.189 -val bool_tp = ResClause.make_fixed_type_const "bool";
   1.190 +val bool_tp = RC.make_fixed_type_const "bool";
   1.191  
   1.192  val app_str = "hAPP";
   1.193  
   1.194 +(*Result of a function type; no need to check that the argument type matches.*)
   1.195 +fun result_type (RC.Comp ("tc_fun", [_, tp2])) = tp2
   1.196 +  | result_type _ = raise ERROR "result_type"
   1.197 +
   1.198  fun type_of_combterm (CombConst(c,tp,_)) = tp
   1.199    | type_of_combterm (CombFree(v,tp)) = tp
   1.200    | type_of_combterm (CombVar(v,tp)) = tp
   1.201 -  | type_of_combterm (CombApp(t1,t2,tp)) = tp;
   1.202 +  | type_of_combterm (CombApp(t1,t2)) = result_type (type_of_combterm t1);
   1.203  
   1.204  (*gets the head of a combinator application, along with the list of arguments*)
   1.205  fun strip_comb u =
   1.206 -    let fun stripc (CombApp(t,u,_), ts) = stripc (t, u::ts)
   1.207 +    let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
   1.208          |   stripc  x =  x
   1.209      in  stripc(u,[])  end;
   1.210  
   1.211 @@ -340,41 +317,41 @@
   1.212        in  wrap_type (c',tp)  end
   1.213    | string_of_combterm1 (CombFree(v,tp)) = wrap_type (v,tp)
   1.214    | string_of_combterm1 (CombVar(v,tp)) = wrap_type (v,tp)
   1.215 -  | string_of_combterm1 (CombApp(t1,t2,tp)) =
   1.216 +  | string_of_combterm1 (CombApp(t1,t2)) =
   1.217        let val s1 = string_of_combterm1 t1
   1.218 -	  val s2 = string_of_combterm1 t2
   1.219 +	  and s2 = string_of_combterm1 t2
   1.220        in
   1.221  	  case !typ_level of
   1.222  	      T_FULL => type_wrapper ^ 
   1.223 -	                ResClause.paren_pack 
   1.224 -	                  [app_str ^ ResClause.paren_pack [s1,s2], 
   1.225 -	                   ResClause.string_of_fol_type tp]
   1.226 -	    | T_PARTIAL => app_str ^ ResClause.paren_pack 
   1.227 -	                     [s1,s2, ResClause.string_of_fol_type (type_of_combterm t1)]
   1.228 -	    | T_NONE => app_str ^ ResClause.paren_pack [s1,s2]
   1.229 +	                RC.paren_pack 
   1.230 +	                  [app_str ^ RC.paren_pack [s1,s2], 
   1.231 +	                   RC.string_of_fol_type (result_type (type_of_combterm t1))]
   1.232 +	    | T_PARTIAL => app_str ^ RC.paren_pack 
   1.233 +	                     [s1,s2, RC.string_of_fol_type (type_of_combterm t1)]
   1.234 +	    | T_NONE => app_str ^ RC.paren_pack [s1,s2]
   1.235  	    | T_CONST => raise ERROR "string_of_combterm1"
   1.236        end;
   1.237  
   1.238  fun rev_apply (v, []) = v
   1.239 -  | rev_apply (v, arg::args) = app_str ^ ResClause.paren_pack [rev_apply (v, args), arg];
   1.240 +  | rev_apply (v, arg::args) = app_str ^ RC.paren_pack [rev_apply (v, args), arg];
   1.241  
   1.242  fun string_apply (v, args) = rev_apply (v, rev args);
   1.243  
   1.244  (*Apply an operator to the argument strings, using either the "apply" operator or
   1.245    direct function application.*)
   1.246 -fun string_of_applic (CombConst(c,tp,tvars), args) =
   1.247 +fun string_of_applic (CombConst(c,_,tvars), args) =
   1.248        let val c = if c = "equal" then "c_fequal" else c
   1.249            val nargs = min_arity_of c
   1.250 -          val args1 = List.take(args, nargs) @ (map ResClause.string_of_fol_type tvars)
   1.251 +          val args1 = List.take(args, nargs) @ (map RC.string_of_fol_type tvars)
   1.252              handle Subscript => raise ERROR ("string_of_applic: " ^ c ^ " has arity " ^
   1.253  					     Int.toString nargs ^ " but is applied to " ^ 
   1.254  					     space_implode ", " args) 
   1.255            val args2 = List.drop(args, nargs)
   1.256        in
   1.257 -	  string_apply (c ^ ResClause.paren_pack args1, args2)
   1.258 +	  string_apply (c ^ RC.paren_pack args1, args2)
   1.259        end
   1.260 -  | string_of_applic (CombFree(v,tp), args) = string_apply (v, args)
   1.261 -  | string_of_applic (CombVar(v,tp), args) = string_apply (v, args)  
   1.262 +  | string_of_applic (CombFree(v,_), args) = string_apply (v, args)
   1.263 +  | string_of_applic (CombVar(v,_), args) = string_apply (v, args)  
   1.264    | string_of_applic _ = raise ERROR "string_of_applic";
   1.265  
   1.266  fun string_of_combterm2 t = 
   1.267 @@ -386,20 +363,20 @@
   1.268  		           | _ => string_of_combterm1 t;
   1.269  
   1.270  (*Boolean-valued terms are here converted to literals.*)
   1.271 -fun boolify t = "hBOOL" ^ ResClause.paren_pack [string_of_combterm t];
   1.272 +fun boolify t = "hBOOL" ^ RC.paren_pack [string_of_combterm t];
   1.273  
   1.274  fun string_of_predicate t = 
   1.275    case t of
   1.276 -      (CombApp(CombApp(CombConst("equal",_,_),t1,_),t2,_)) =>
   1.277 +      (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
   1.278  	  (*DFG only: new TPTP prefers infix equality*)
   1.279 -	  ("equal" ^ ResClause.paren_pack [string_of_combterm t1, string_of_combterm t2])
   1.280 +	  ("equal" ^ RC.paren_pack [string_of_combterm t1, string_of_combterm t2])
   1.281      | _ => 
   1.282            case #1 (strip_comb t) of
   1.283                CombConst(c,_,_) => if needs_hBOOL c then boolify t else string_of_combterm t
   1.284              | _ => boolify t;
   1.285  
   1.286  fun string_of_clausename (cls_id,ax_name) = 
   1.287 -    ResClause.clause_prefix ^ ResClause.ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   1.288 +    RC.clause_prefix ^ RC.ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   1.289  
   1.290  fun string_of_type_clsname (cls_id,ax_name,idx) = 
   1.291      string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
   1.292 @@ -411,10 +388,10 @@
   1.293    let val eqop = if pol then " = " else " != "
   1.294    in  string_of_combterm t1 ^ eqop ^ string_of_combterm t2  end;
   1.295  
   1.296 -fun tptp_literal (Literal(pol, CombApp(CombApp(CombConst("equal",_,_),t1,_),t2,_))) = 
   1.297 +fun tptp_literal (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) = 
   1.298        tptp_of_equality pol (t1,t2)
   1.299    | tptp_literal (Literal(pol,pred)) = 
   1.300 -      ResClause.tptp_sign pol (string_of_predicate pred);
   1.301 +      RC.tptp_sign pol (string_of_predicate pred);
   1.302   
   1.303  (*Given a clause, returns its literals paired with a list of literals concerning TFrees;
   1.304    the latter should only occur in conjecture clauses.*)
   1.305 @@ -422,17 +399,17 @@
   1.306      let val lits = map tptp_literal (#literals cls)
   1.307  	val ctvar_lits_strs =
   1.308  	    case !typ_level of T_NONE => []
   1.309 -	      | _ => map ResClause.tptp_of_typeLit (#ctvar_type_literals cls)
   1.310 +	      | _ => map RC.tptp_of_typeLit (#ctvar_type_literals cls)
   1.311  	val ctfree_lits = 
   1.312  	    case !typ_level of T_NONE => []
   1.313 -	      | _ => map ResClause.tptp_of_typeLit (#ctfree_type_literals cls)
   1.314 +	      | _ => map RC.tptp_of_typeLit (#ctfree_type_literals cls)
   1.315      in
   1.316  	(ctvar_lits_strs @ lits, ctfree_lits)
   1.317      end; 
   1.318      
   1.319  fun clause2tptp (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   1.320      let val (lits,ctfree_lits) = tptp_type_lits cls
   1.321 -	val cls_str = ResClause.gen_tptp_cls(clause_id,axiom_name,kind,lits)
   1.322 +	val cls_str = RC.gen_tptp_cls(clause_id,axiom_name,kind,lits)
   1.323      in
   1.324  	(cls_str,ctfree_lits)
   1.325      end;
   1.326 @@ -440,42 +417,42 @@
   1.327  
   1.328  (*** dfg format ***)
   1.329  
   1.330 -fun dfg_literal (Literal(pol,pred)) = ResClause.dfg_sign pol (string_of_predicate pred);
   1.331 +fun dfg_literal (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate pred);
   1.332  
   1.333  fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) = 
   1.334    let val lits = map dfg_literal literals
   1.335 -      val (tvar_lits,tfree_lits) = ResClause.add_typs_aux ctypes_sorts
   1.336 +      val (tvar_lits,tfree_lits) = RC.add_typs_aux ctypes_sorts
   1.337        val tvar_lits_strs = 
   1.338  	  case !typ_level of T_NONE => [] 
   1.339 -	      | _ => map ResClause.dfg_of_typeLit tvar_lits
   1.340 +	      | _ => map RC.dfg_of_typeLit tvar_lits
   1.341        val tfree_lits =
   1.342            case !typ_level of T_NONE => []
   1.343 -	      | _ => map ResClause.dfg_of_typeLit tfree_lits 
   1.344 +	      | _ => map RC.dfg_of_typeLit tfree_lits 
   1.345    in
   1.346        (tvar_lits_strs @ lits, tfree_lits)
   1.347    end; 
   1.348  
   1.349 -fun get_uvars (CombConst(_,_,_)) vars = vars
   1.350 -  | get_uvars (CombFree(_,_)) vars = vars
   1.351 -  | get_uvars (CombVar(v,tp)) vars = (v::vars)
   1.352 -  | get_uvars (CombApp(P,Q,tp)) vars = get_uvars P (get_uvars Q vars);
   1.353 +fun get_uvars (CombConst _) vars = vars
   1.354 +  | get_uvars (CombFree _) vars = vars
   1.355 +  | get_uvars (CombVar(v,_)) vars = (v::vars)
   1.356 +  | get_uvars (CombApp(P,Q)) vars = get_uvars P (get_uvars Q vars);
   1.357  
   1.358  fun get_uvars_l (Literal(_,c)) = get_uvars c [];
   1.359  
   1.360 -fun dfg_vars (Clause {literals,...}) = ResClause.union_all (map get_uvars_l literals);
   1.361 +fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals);
   1.362   
   1.363  fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   1.364      let val (lits,tfree_lits) = dfg_clause_aux cls 
   1.365          val vars = dfg_vars cls
   1.366 -        val tvars = ResClause.get_tvar_strs ctypes_sorts
   1.367 -	val knd = ResClause.name_of_kind kind
   1.368 +        val tvars = RC.get_tvar_strs ctypes_sorts
   1.369 +	val knd = RC.name_of_kind kind
   1.370  	val lits_str = commas lits
   1.371 -	val cls_str = ResClause.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars) 
   1.372 +	val cls_str = RC.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars) 
   1.373      in (cls_str, tfree_lits) end;
   1.374  
   1.375  (** For DFG format: accumulate function and predicate declarations **)
   1.376  
   1.377 -fun addtypes tvars tab = foldl ResClause.add_foltype_funcs tab tvars;
   1.378 +fun addtypes tvars tab = foldl RC.add_foltype_funcs tab tvars;
   1.379  
   1.380  fun add_decls (CombConst(c,_,tvars), (funcs,preds)) =
   1.381        if c = "equal" then (addtypes tvars funcs, preds)
   1.382 @@ -490,10 +467,10 @@
   1.383                 end
   1.384             | _ => (addtypes tvars (Symtab.update(c,0) funcs), preds))
   1.385    | add_decls (CombFree(v,ctp), (funcs,preds)) = 
   1.386 -      (ResClause.add_foltype_funcs (ctp,Symtab.update (v,0) funcs), preds)
   1.387 +      (RC.add_foltype_funcs (ctp,Symtab.update (v,0) funcs), preds)
   1.388    | add_decls (CombVar(_,ctp), (funcs,preds)) = 
   1.389 -      (ResClause.add_foltype_funcs (ctp,funcs), preds)
   1.390 -  | add_decls (CombApp(P,Q,_),decls) = add_decls(P,add_decls (Q,decls));
   1.391 +      (RC.add_foltype_funcs (ctp,funcs), preds)
   1.392 +  | add_decls (CombApp(P,Q),decls) = add_decls(P,add_decls (Q,decls));
   1.393  
   1.394  fun add_literal_decls (Literal(_,c), decls) = add_decls (c,decls);
   1.395  
   1.396 @@ -507,19 +484,19 @@
   1.397        val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
   1.398        val (functab,predtab) = (foldl add_clause_decls (init_functab, init_predtab) clauses)
   1.399    in
   1.400 -      (Symtab.dest (foldl ResClause.add_arityClause_funcs functab arity_clauses), 
   1.401 +      (Symtab.dest (foldl RC.add_arityClause_funcs functab arity_clauses), 
   1.402         Symtab.dest predtab)
   1.403    end;
   1.404  
   1.405  fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
   1.406 -  foldl ResClause.add_type_sort_preds preds ctypes_sorts
   1.407 +  foldl RC.add_type_sort_preds preds ctypes_sorts
   1.408    handle Symtab.DUP a => raise ERROR ("predicate " ^ a ^ " has multiple arities")
   1.409  
   1.410  (*Higher-order clauses have only the predicates hBOOL and type classes.*)
   1.411  fun preds_of_clauses clauses clsrel_clauses arity_clauses = 
   1.412      Symtab.dest
   1.413 -	(foldl ResClause.add_classrelClause_preds 
   1.414 -	       (foldl ResClause.add_arityClause_preds
   1.415 +	(foldl RC.add_classrelClause_preds 
   1.416 +	       (foldl RC.add_arityClause_preds
   1.417  		      (foldl add_clause_preds Symtab.empty clauses) 
   1.418  		      arity_clauses)
   1.419  	       clsrel_clauses)
   1.420 @@ -542,7 +519,7 @@
   1.421                                 | SOME n => Symtab.update (c,n+1) ct)
   1.422    | count_combterm (CombFree(v,tp), ct) = ct
   1.423    | count_combterm (CombVar(v,tp), ct) = ct
   1.424 -  | count_combterm (CombApp(t1,t2,tp), ct) = count_combterm(t1, count_combterm(t2, ct));
   1.425 +  | count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct));
   1.426  
   1.427  fun count_literal (Literal(_,t), ct) = count_combterm(t,ct);
   1.428  
   1.429 @@ -622,14 +599,14 @@
   1.430  	val helper_clauses = get_helper_clauses (conjectures, axclauses, user_lemmas)
   1.431  	val _ = count_constants (conjectures, axclauses, helper_clauses);
   1.432  	val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp conjectures)
   1.433 -	val tfree_clss = map ResClause.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
   1.434 +	val tfree_clss = map RC.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
   1.435          val out = TextIO.openOut filename
   1.436      in
   1.437  	List.app (curry TextIO.output out o #1 o clause2tptp) axclauses;
   1.438 -	ResClause.writeln_strs out tfree_clss;
   1.439 -	ResClause.writeln_strs out tptp_clss;
   1.440 -	List.app (curry TextIO.output out o ResClause.tptp_classrelClause) classrel_clauses;
   1.441 -	List.app (curry TextIO.output out o ResClause.tptp_arity_clause) arity_clauses;
   1.442 +	RC.writeln_strs out tfree_clss;
   1.443 +	RC.writeln_strs out tptp_clss;
   1.444 +	List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses;
   1.445 +	List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses;
   1.446  	List.app (curry TextIO.output out o #1 o clause2tptp) helper_clauses;
   1.447  	TextIO.closeOut out;
   1.448  	clnames
   1.449 @@ -647,25 +624,25 @@
   1.450  	val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
   1.451  	and probname = Path.implode (Path.base (Path.explode filename))
   1.452  	val axstrs = map (#1 o clause2dfg) axclauses
   1.453 -	val tfree_clss = map ResClause.dfg_tfree_clause (ResClause.union_all tfree_litss)
   1.454 +	val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
   1.455  	val out = TextIO.openOut filename
   1.456  	val helper_clauses_strs = map (#1 o clause2dfg) helper_clauses
   1.457  	val (funcs,cl_preds) = decls_of_clauses (helper_clauses @ conjectures @ axclauses) arity_clauses
   1.458  	and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
   1.459      in
   1.460 -	TextIO.output (out, ResClause.string_of_start probname); 
   1.461 -	TextIO.output (out, ResClause.string_of_descrip probname); 
   1.462 -	TextIO.output (out, ResClause.string_of_symbols 
   1.463 -	                      (ResClause.string_of_funcs funcs) 
   1.464 -	                      (ResClause.string_of_preds (cl_preds @ ty_preds))); 
   1.465 +	TextIO.output (out, RC.string_of_start probname); 
   1.466 +	TextIO.output (out, RC.string_of_descrip probname); 
   1.467 +	TextIO.output (out, RC.string_of_symbols 
   1.468 +	                      (RC.string_of_funcs funcs) 
   1.469 +	                      (RC.string_of_preds (cl_preds @ ty_preds))); 
   1.470  	TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
   1.471 -	ResClause.writeln_strs out axstrs;
   1.472 -	List.app (curry TextIO.output out o ResClause.dfg_classrelClause) classrel_clauses;
   1.473 -	List.app (curry TextIO.output out o ResClause.dfg_arity_clause) arity_clauses;
   1.474 -	ResClause.writeln_strs out helper_clauses_strs;
   1.475 +	RC.writeln_strs out axstrs;
   1.476 +	List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses;
   1.477 +	List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses;
   1.478 +	RC.writeln_strs out helper_clauses_strs;
   1.479  	TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
   1.480 -	ResClause.writeln_strs out tfree_clss;
   1.481 -	ResClause.writeln_strs out dfg_clss;
   1.482 +	RC.writeln_strs out tfree_clss;
   1.483 +	RC.writeln_strs out dfg_clss;
   1.484  	TextIO.output (out, "end_of_list.\n\n");
   1.485  	(*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
   1.486  	TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n");