src/HOL/Tools/res_clause.ML
changeset 18856 4669dec681f4
parent 18798 ca02a2077955
child 18863 a113b6839df1
     1.1 --- a/src/HOL/Tools/res_clause.ML	Mon Jan 30 12:20:06 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Mon Jan 30 15:31:31 2006 +0100
     1.3 @@ -25,7 +25,6 @@
     1.4    val isTaut : clause -> bool
     1.5    val num_of_clauses : clause -> int
     1.6  
     1.7 -  val clause2dfg : clause -> string * string list
     1.8    val clauses2dfg : string -> clause list -> clause list -> string
     1.9    val tfree_dfg_clause : string -> string
    1.10  
    1.11 @@ -63,7 +62,7 @@
    1.12    type typ_var
    1.13    val mk_typ_var_sort : Term.typ -> typ_var * sort
    1.14    type type_literal
    1.15 -  val add_typs_aux2 : (typ_var * string list) list -> type_literal list * type_literal list
    1.16 +  val add_typs_aux : (typ_var * string list) list -> type_literal list * type_literal list
    1.17    val gen_tptp_cls : int * string * string * string -> string
    1.18    val gen_tptp_type_cls : int * string * string * string * int -> string
    1.19    val tptp_of_typeLit : type_literal -> string
    1.20 @@ -228,11 +227,8 @@
    1.21  fun string_of_fol_type (AtomV x) = x
    1.22    | string_of_fol_type (AtomF x) = x
    1.23    | string_of_fol_type (Comp(tcon,tps)) = 
    1.24 -    let val tstrs = map string_of_fol_type tps
    1.25 -    in
    1.26 -	tcon ^ (paren_pack tstrs)
    1.27 -    end;
    1.28 -
    1.29 +      tcon ^ (paren_pack (map string_of_fol_type tps));
    1.30 +      
    1.31  fun mk_fol_type ("Var",x,_) = AtomV(x)
    1.32    | mk_fol_type ("Fixed",x,_) = AtomF(x)
    1.33    | mk_fol_type ("Comp",con,args) = Comp(con,args)
    1.34 @@ -241,9 +237,9 @@
    1.35  (*First string is the type class; the second is a TVar or TFfree*)
    1.36  datatype type_literal = LTVar of string * string | LTFree of string * string;
    1.37  
    1.38 -datatype folTerm = UVar of string * fol_type
    1.39 -                 | Fun of string * fol_type list * folTerm list;
    1.40 -datatype predicate = Predicate of pred_name * fol_type list * folTerm list;
    1.41 +datatype fol_term = UVar of string * fol_type
    1.42 +                 | Fun of string * fol_type list * fol_term list;
    1.43 +datatype predicate = Predicate of pred_name * fol_type list * fol_term list;
    1.44  
    1.45  datatype literal = Literal of polarity * predicate * tag;
    1.46  
    1.47 @@ -251,8 +247,7 @@
    1.48    | mk_typ_var_sort (TVar(v,s)) = (FOLTVar v,s);
    1.49  
    1.50  
    1.51 -
    1.52 -(* ML datatype used to repsent one single clause: disjunction of literals. *)
    1.53 +(*A clause has first-order literals and other, type-related literals*)
    1.54  datatype clause = 
    1.55  	 Clause of {clause_id: clause_id,
    1.56  		    axiom_name: axiom_name,
    1.57 @@ -260,40 +255,31 @@
    1.58  		    literals: literal list,
    1.59  		    types_sorts: (typ_var * sort) list, 
    1.60                      tvar_type_literals: type_literal list, 
    1.61 -                    tfree_type_literals: type_literal list,
    1.62 -                    predicates: (string*int) list};
    1.63 -
    1.64 +                    tfree_type_literals: type_literal list};
    1.65  
    1.66  exception CLAUSE of string * term;
    1.67  
    1.68 -fun predicate_name (Predicate(predname,_,_)) = predname;
    1.69 -
    1.70 -
    1.71 -(*** make clauses ***)
    1.72 -
    1.73 -fun isFalse (Literal (pol,Predicate(a,_,[]),_)) =
    1.74 -      (pol andalso a = "c_False") orelse
    1.75 -      (not pol andalso a = "c_True")
    1.76 +fun isFalse (Literal (pol,Predicate(pname,_,[]),_)) =
    1.77 +      (pol andalso pname = "c_False") orelse
    1.78 +      (not pol andalso pname = "c_True")
    1.79    | isFalse _ = false;
    1.80  
    1.81 -fun isTrue (Literal (pol,Predicate(a,_,[]),_)) =
    1.82 -      (pol andalso a = "c_True") orelse
    1.83 -      (not pol andalso a = "c_False")
    1.84 +fun isTrue (Literal (pol,Predicate(pname,_,[]),_)) =
    1.85 +      (pol andalso pname = "c_True") orelse
    1.86 +      (not pol andalso pname = "c_False")
    1.87    | isTrue _ = false;
    1.88    
    1.89  fun isTaut (Clause {literals,...}) = exists isTrue literals;  
    1.90  
    1.91  fun make_clause (clause_id,axiom_name,kind,literals,
    1.92 -                 types_sorts,tvar_type_literals,
    1.93 -                 tfree_type_literals,predicates) =
    1.94 +                 types_sorts,tvar_type_literals,tfree_type_literals) =
    1.95    if forall isFalse literals 
    1.96    then error "Problem too trivial for resolution (empty clause)"
    1.97    else
    1.98       Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind, 
    1.99               literals = literals, types_sorts = types_sorts,
   1.100               tvar_type_literals = tvar_type_literals,
   1.101 -             tfree_type_literals = tfree_type_literals,
   1.102 -             predicates = predicates};
   1.103 +             tfree_type_literals = tfree_type_literals};
   1.104  
   1.105  
   1.106  (** Some Clause destructor functions **)
   1.107 @@ -304,8 +290,6 @@
   1.108  
   1.109  fun get_clause_id (Clause cls) = #clause_id cls;
   1.110  
   1.111 -fun preds_of_cls (Clause cls) = #predicates cls;
   1.112 -
   1.113  
   1.114  (*Declarations of the current theory--to allow suppressing types.*)
   1.115  val const_typargs = ref (Library.K [] : (string*typ -> typ list));
   1.116 @@ -357,6 +341,8 @@
   1.117         else (make_fixed_var x, ([],[]))
   1.118    | fun_name_type f args = raise CLAUSE("Function Not First Order 1", f);
   1.119  
   1.120 +(*Convert a term to a fol_term while accumulating sort constraints on the TFrees and
   1.121 +  TVars it contains.*)    
   1.122  fun term_of (Var(ind_nm,T)) = 
   1.123        let val (folType,ts) = type_of T
   1.124        in (UVar(make_schematic_var ind_nm, folType), ts) end
   1.125 @@ -376,29 +362,22 @@
   1.126        end
   1.127  and terms_of ts = ListPair.unzip (map term_of ts)
   1.128  
   1.129 -
   1.130 +(*Create a predicate value, again accumulating sort constraints.*)    
   1.131  fun pred_of (Const("op =", typ), args) =
   1.132        let val arg_typ = eq_arg_type typ 
   1.133  	  val (args',ts) = terms_of args
   1.134  	  val equal_name = make_fixed_const "op ="
   1.135        in
   1.136  	  (Predicate(equal_name,[arg_typ],args'),
   1.137 -	   union_all ts, 
   1.138 -	   [((make_fixed_var equal_name), 2)])
   1.139 +	   union_all ts)
   1.140        end
   1.141    | pred_of (pred,args) = 
   1.142 -      let val (predName, (predType,ts1)) = pred_name_type pred
   1.143 +      let val (pname, (predType,ts1)) = pred_name_type pred
   1.144  	  val (args',ts2) = terms_of args
   1.145 -	  val ts3 = union_all (ts1::ts2)
   1.146 -	  val arity = 
   1.147 -	    case pred of
   1.148 -		Const (c,T) => num_typargs(c,T) + length args
   1.149 -	      | _ => length args
   1.150        in
   1.151 -	  (Predicate(predName,predType,args'), ts3, [(predName, arity)])
   1.152 +	  (Predicate(pname,predType,args'), union_all (ts1::ts2))
   1.153        end;
   1.154  
   1.155 -
   1.156  (*Treatment of literals, possibly negated or tagged*)
   1.157  fun predicate_of ((Const("Not",_) $ P), polarity, tag) =
   1.158        predicate_of (P, not polarity, tag)
   1.159 @@ -408,21 +387,16 @@
   1.160          (pred_of (strip_comb term), polarity, tag);
   1.161  
   1.162  fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P
   1.163 -  | literals_of_term1 (args as (lits, ts, preds)) (Const("op |",_) $ P $ Q) = 
   1.164 -      let val (lits', ts', preds') = literals_of_term1 args P
   1.165 +  | literals_of_term1 args (Const("op |",_) $ P $ Q) = 
   1.166 +      literals_of_term1 (literals_of_term1 args P) Q
   1.167 +  | literals_of_term1 (lits, ts) P =
   1.168 +      let val ((pred, ts'), polarity, tag) = predicate_of (P,true,false)
   1.169 +	  val lits' = Literal(polarity,pred,tag) :: lits
   1.170        in
   1.171 -	  literals_of_term1 (lits', ts', preds' union preds) Q
   1.172 -      end
   1.173 -  | literals_of_term1 (lits, ts, preds) P =
   1.174 -      let val ((pred, ts', preds'), pol, tag) = predicate_of (P,true,false)
   1.175 -	  val lits' = Literal(pol,pred,tag) :: lits
   1.176 -      in
   1.177 -	  (lits', ts union ts', preds' union preds)
   1.178 +	  (lits', ts union ts')
   1.179        end;
   1.180  
   1.181 -
   1.182 -val literals_of_term = literals_of_term1 ([],[],[]);
   1.183 -
   1.184 +val literals_of_term = literals_of_term1 ([],[]);
   1.185  
   1.186  
   1.187  fun list_ord _ ([],[]) = EQUAL
   1.188 @@ -471,17 +445,12 @@
   1.189  
   1.190  
   1.191  
   1.192 -fun predicate_ord (Predicate(predname1,ftyps1,ftms1),Predicate(predname2,ftyps2,ftms2)) = 
   1.193 -    let val predname_ord = string_ord (predname1,predname2)
   1.194 -    in
   1.195 -	case predname_ord of EQUAL => 
   1.196 -			     let val ftms_ord = terms_ord(ftms1,ftms2)
   1.197 -			     in
   1.198 -				 case ftms_ord of EQUAL => types_ord(ftyps1,ftyps2)
   1.199 -						| _ => ftms_ord
   1.200 -			     end
   1.201 -			   | _ => predname_ord
   1.202 -    end;
   1.203 +fun predicate_ord (Predicate(pname1,ftyps1,ftms1),Predicate(pname2,ftyps2,ftms2)) = 
   1.204 +  case string_ord (pname1,pname2) of
   1.205 +       EQUAL => (case terms_ord(ftms1,ftms2) of EQUAL => types_ord(ftyps1,ftyps2)
   1.206 +				              | ftms_ord => ftms_ord)
   1.207 +     | pname_ord => pname_ord
   1.208 +			   
   1.209  
   1.210  fun literal_ord (Literal(false,_,_),Literal(true,_,_)) = LESS
   1.211    | literal_ord (Literal(true,_,_),Literal(false,_,_)) = GREATER
   1.212 @@ -556,9 +525,9 @@
   1.213        end;
   1.214  					     
   1.215  
   1.216 -fun pred_eq (Predicate(predname1,tps1,tms1),Predicate(predname2,tps2,tms2)) vtvars =
   1.217 +fun pred_eq (Predicate(pname1,tps1,tms1),Predicate(pname2,tps2,tms2)) vtvars =
   1.218      let val (eq1,vtvars1) = 
   1.219 -	    if (predname1 = predname2) then terms_eq (tms1,tms2) vtvars
   1.220 +	    if (pname1 = pname2) then terms_eq (tms1,tms2) vtvars
   1.221  	    else (false,vtvars)
   1.222  	val (eq2,vtvars2) = 
   1.223  	    if eq1 then types_eq (tps1,tps2) vtvars1
   1.224 @@ -622,38 +591,22 @@
   1.225  
   1.226  (*Given a list of sorted type variables, return two separate lists.
   1.227    The first is for TVars, the second for TFrees.*)
   1.228 -fun add_typs_aux [] preds  = ([],[], preds)
   1.229 -  | add_typs_aux ((FOLTVar indx,s)::tss) preds = 
   1.230 +fun add_typs_aux [] = ([],[])
   1.231 +  | add_typs_aux ((FOLTVar indx,s)::tss) = 
   1.232        let val vs = sorts_on_typs (FOLTVar indx, s)
   1.233 -          val preds' = (map pred_of_sort vs)@preds
   1.234 -	  val (vss,fss, preds'') = add_typs_aux tss preds'
   1.235 +	  val (vss,fss) = add_typs_aux tss
   1.236        in
   1.237 -	  (vs union vss, fss, preds'')
   1.238 +	  (vs union vss, fss)
   1.239        end
   1.240 -  | add_typs_aux ((FOLTFree x,s)::tss) preds  =
   1.241 +  | add_typs_aux ((FOLTFree x,s)::tss) =
   1.242        let val fs = sorts_on_typs (FOLTFree x, s)
   1.243 -          val preds' = (map pred_of_sort fs)@preds
   1.244 -	  val (vss,fss, preds'') = add_typs_aux tss preds'
   1.245 +	  val (vss,fss) = add_typs_aux tss
   1.246        in
   1.247 -	  (vss, fs union fss, preds'')
   1.248 +	  (vss, fs union fss)
   1.249        end;
   1.250  
   1.251 -fun add_typs_aux2 [] = ([],[])
   1.252 -  | add_typs_aux2 ((FOLTVar indx,s)::tss) =
   1.253 -    let val vs = sorts_on_typs (FOLTVar indx,s)
   1.254 -	val (vss,fss) = add_typs_aux2 tss
   1.255 -    in
   1.256 -	(vs union vss,fss)
   1.257 -    end
   1.258 -  | add_typs_aux2 ((FOLTFree x,s)::tss) =
   1.259 -    let val fs = sorts_on_typs (FOLTFree x,s)
   1.260 -	val (vss,fss) = add_typs_aux2 tss
   1.261 -    in
   1.262 -	(vss,fs union fss)
   1.263 -    end;
   1.264  
   1.265 -
   1.266 -fun add_typs (Clause cls) preds  = add_typs_aux (#types_sorts cls) preds 
   1.267 +fun add_typs (Clause cls) = add_typs_aux (#types_sorts cls)  
   1.268  
   1.269  
   1.270  (** make axiom clauses, hypothesis clauses and conjecture clauses. **)
   1.271 @@ -667,12 +620,12 @@
   1.272    | get_tvar_strs((FOLTFree x,s)::tss) = distinct (get_tvar_strs tss)
   1.273  
   1.274  fun make_axiom_clause_thm thm (ax_name,cls_id) =
   1.275 -    let val (lits,types_sorts, preds) = literals_of_term (prop_of thm)
   1.276 +    let val (lits,types_sorts) = literals_of_term (prop_of thm)
   1.277  	val lits' = sort_lits lits
   1.278 -	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds 
   1.279 +	val (tvar_lits,tfree_lits) = add_typs_aux types_sorts  
   1.280      in 
   1.281  	make_clause(cls_id,ax_name,Axiom,
   1.282 -	            lits',types_sorts,tvar_lits,tfree_lits,preds)
   1.283 +	            lits',types_sorts,tvar_lits,tfree_lits)
   1.284      end;
   1.285  
   1.286  
   1.287 @@ -680,11 +633,11 @@
   1.288  fun make_conjecture_clause n t =
   1.289      let val _ = check_is_fol_term t
   1.290  	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Goal is not FOL",t)
   1.291 -	val (lits,types_sorts, preds) = literals_of_term t
   1.292 -	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds 
   1.293 +	val (lits,types_sorts) = literals_of_term t
   1.294 +	val (tvar_lits,tfree_lits) = add_typs_aux types_sorts 
   1.295      in
   1.296  	make_clause(n,"conjecture",Conjecture,
   1.297 -	            lits,types_sorts,tvar_lits,tfree_lits,preds)
   1.298 +	            lits,types_sorts,tvar_lits,tfree_lits)
   1.299      end;
   1.300      
   1.301  fun make_conjecture_clauses_aux _ [] = []
   1.302 @@ -698,17 +651,15 @@
   1.303  fun make_axiom_clause term (ax_name,cls_id) =
   1.304      let val _ = check_is_fol_term term 
   1.305  	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Axiom is not FOL", term) 
   1.306 -	val (lits,types_sorts, preds) = literals_of_term term
   1.307 +	val (lits,types_sorts) = literals_of_term term
   1.308  	val lits' = sort_lits lits
   1.309 -	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds
   1.310 +	val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
   1.311      in 
   1.312  	make_clause(cls_id,ax_name,Axiom,
   1.313 -	            lits',types_sorts,tvar_lits,tfree_lits,preds)
   1.314 +	            lits',types_sorts,tvar_lits,tfree_lits)
   1.315      end;
   1.316  
   1.317  
   1.318 -
   1.319 - 
   1.320  (**** Isabelle arities ****)
   1.321  
   1.322  exception ARCLAUSE of string;
   1.323 @@ -856,7 +807,7 @@
   1.324      end;
   1.325  
   1.326  fun dfg_of_typeLit (LTVar (s,ty)) = "not(" ^ s ^ "(" ^ ty ^ "))"
   1.327 -  | dfg_of_typeLit (LTFree (s,ty)) = "(" ^ s ^ "(" ^ ty ^ "))";
   1.328 +  | dfg_of_typeLit (LTFree (s,ty)) = s ^ "(" ^ ty ^ ")";
   1.329   
   1.330  (*Make the string of universal quantifiers for a clause*)
   1.331  fun forall_open ([],[]) = ""
   1.332 @@ -870,6 +821,7 @@
   1.333      "or(" ^ lits ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ 
   1.334      string_of_clausename (cls_id,ax_name) ^  ").";
   1.335  
   1.336 +(*FIXME: UNUSED*)
   1.337  fun gen_dfg_type_cls (cls_id,ax_name,knd,tfree_lit,idx,tvars,vars) = 
   1.338      "clause( %(" ^ knd ^ ")\n" ^ forall_open(vars,tvars) ^ 
   1.339      "or( " ^ tfree_lit ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ 
   1.340 @@ -889,7 +841,7 @@
   1.341  
   1.342  
   1.343  fun dfg_folterms (Literal(pol,pred,tag)) = 
   1.344 -  let val Predicate (predname, _, folterms) = pred
   1.345 +  let val Predicate (_, _, folterms) = pred
   1.346    in  folterms  end
   1.347  
   1.348  fun get_uvars (UVar(a,typ)) = [a] 
   1.349 @@ -919,7 +871,6 @@
   1.350              (*"lits" includes the typing assumptions (TVars)*)
   1.351          val vars = dfg_vars cls
   1.352          val tvars = get_tvar_strs types_sorts
   1.353 -        val preds = preds_of_cls cls
   1.354  	val knd = name_of_kind kind
   1.355  	val lits_str = commas lits
   1.356  	val cls_str = gen_dfg_cls(clause_id,axiom_name,knd,lits_str,tvars,vars) 
   1.357 @@ -927,11 +878,11 @@
   1.358  
   1.359  fun string_of_arity (name, num) =  "(" ^ name ^ "," ^ Int.toString num ^ ")"
   1.360  
   1.361 -fun string_of_preds preds = 
   1.362 -  "predicates[" ^ commas(map string_of_arity preds) ^ "].\n";
   1.363 +fun string_of_preds [] = ""
   1.364 +  | string_of_preds preds = "predicates[" ^ commas(map string_of_arity preds) ^ "].\n";
   1.365  
   1.366 -fun string_of_funcs funcs =
   1.367 -  "functions[" ^ commas(map string_of_arity funcs) ^ "].\n" ;
   1.368 +fun string_of_funcs [] = ""
   1.369 +  | string_of_funcs funcs = "functions[" ^ commas(map string_of_arity funcs) ^ "].\n" ;
   1.370  
   1.371  fun string_of_symbols predstr funcstr = 
   1.372    "list_of_symbols.\n" ^ predstr  ^ funcstr  ^ "end_of_list.\n\n";
   1.373 @@ -953,8 +904,7 @@
   1.374      let val axstrs_tfrees = (map clause2dfg axioms)
   1.375  	val (axstrs, atfrees) = ListPair.unzip axstrs_tfrees
   1.376          val axstr = (space_implode "\n" axstrs) ^ "\n\n"
   1.377 -        val conjstrs_tfrees = (map clause2dfg conjectures)
   1.378 -	val (conjstrs, atfrees) = ListPair.unzip conjstrs_tfrees
   1.379 +	val (conjstrs, atfrees) = ListPair.unzip (map clause2dfg conjectures)
   1.380          val tfree_clss = map tfree_dfg_clause (union_all atfrees) 
   1.381          val conjstr = (space_implode "\n" (tfree_clss@conjstrs)) ^ "\n\n"
   1.382          val funcstr = string_of_funcs funcs
   1.383 @@ -966,22 +916,46 @@
   1.384         string_of_conjectures conjstr ^ "end_problem.\n"
   1.385      end;
   1.386     
   1.387 -fun add_clause_preds (cls,preds) = (preds_of_cls cls) union preds;
   1.388 -val preds_of_clauses = foldl add_clause_preds []
   1.389 +
   1.390 +(*** Find all occurrences of predicates in types, terms, literals... ***)
   1.391 +
   1.392 +(*FIXME: multiple-arity checking doesn't work, as update_new is the wrong 
   1.393 +  function (it flags repeated declarations of a function, even with the same arity)*)
   1.394 +
   1.395 +fun update_many (tab, keypairs) = foldl (uncurry Symtab.update) tab keypairs;
   1.396 +
   1.397 +fun add_predicate_preds (Predicate(pname,tys,tms), preds) = 
   1.398 +  if pname = "equal" then preds (*equality is built-in and requires no declaration*)
   1.399 +  else Symtab.update (pname, length tys + length tms) preds
   1.400 +
   1.401 +fun add_literal_preds (Literal(_,pred,_), preds) = add_predicate_preds (pred,preds)
   1.402  
   1.403 -(*FIXME: can replace expensive list operations (ins) by trees (symtab)*)
   1.404 +fun add_type_sort_preds ((FOLTVar indx,s), preds) = 
   1.405 +      update_many (preds, map pred_of_sort (sorts_on_typs (FOLTVar indx, s)))
   1.406 +  | add_type_sort_preds ((FOLTFree x,s), preds) =
   1.407 +      update_many (preds, map pred_of_sort (sorts_on_typs (FOLTFree x, s)));
   1.408 +
   1.409 +fun add_clause_preds (Clause {literals, types_sorts, ...}, preds) =
   1.410 +  foldl add_literal_preds (foldl add_type_sort_preds preds types_sorts) literals
   1.411 +  handle Symtab.DUP a => raise ERROR ("predicate " ^ a ^ " has multiple arities")
   1.412 +
   1.413 +val preds_of_clauses = Symtab.dest o (foldl add_clause_preds Symtab.empty)
   1.414 +
   1.415 +
   1.416 +(*** Find all occurrences of functions in types, terms, literals... ***)
   1.417  
   1.418  fun add_foltype_funcs (AtomV _, funcs) = funcs
   1.419 -  | add_foltype_funcs (AtomF a, funcs) = (a,0) ins funcs
   1.420 +  | add_foltype_funcs (AtomF a, funcs) = Symtab.update (a,0) funcs
   1.421    | add_foltype_funcs (Comp(a,tys), funcs) = 
   1.422 -      foldl add_foltype_funcs ((a, length tys) ins funcs) tys;
   1.423 +      foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys;
   1.424  
   1.425  fun add_folterm_funcs (UVar _, funcs) = funcs
   1.426 -  | add_folterm_funcs (Fun(a,tys,[]), funcs) = (a,0) ins funcs
   1.427 +  | add_folterm_funcs (Fun(a,tys,[]), funcs) = Symtab.update (a,0) funcs
   1.428        (*A constant is a special case: it has no type argument even if overloaded*)
   1.429    | add_folterm_funcs (Fun(a,tys,tms), funcs) = 
   1.430        foldl add_foltype_funcs 
   1.431 -	    (foldl add_folterm_funcs ((a, length tys + length tms) ins funcs) tms) 
   1.432 +	    (foldl add_folterm_funcs (Symtab.update (a, length tys + length tms) funcs) 
   1.433 +	           tms) 
   1.434  	    tys
   1.435  
   1.436  fun add_predicate_funcs (Predicate(_,tys,tms), funcs) = 
   1.437 @@ -990,9 +964,10 @@
   1.438  fun add_literal_funcs (Literal(_,pred,_), funcs) = add_predicate_funcs (pred,funcs)
   1.439  
   1.440  fun add_clause_funcs (Clause {literals, ...}, funcs) =
   1.441 -  foldl add_literal_funcs funcs literals;
   1.442 +  foldl add_literal_funcs funcs literals
   1.443 +  handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities")
   1.444  
   1.445 -val funcs_of_clauses = foldl add_clause_funcs []
   1.446 +val funcs_of_clauses = Symtab.dest o (foldl add_clause_funcs Symtab.empty)
   1.447  
   1.448  
   1.449  fun clauses2dfg probname axioms conjectures =