Lines Matching defs:fns
247 let fun munge fns [] vars bcases = ([],bcases)
248 | munge fns (h::t) vars bcases =
250 if mem f fns
251 then (append(single h) ## I) (munge fns t vars bcases)
256 (munge (f::fns) t (h0_vars@vars) (h0::bcases))
286 val (fns,args) = unzip(map strip_comb L)
287 val ufns = mk_set fns (* unique fns, should all be variables *)
294 val fns' = map (mysubst thetaL) fns
295 val L' = map2 (curry list_mk_comb) fns' args