Lines Matching defs:cl
174 fun fact_to_vthm (FACT (cl, thk)) = (clause_vars cl, force thk);
236 fn FACT (cl, th) =>
238 fun process (sub, cl', vf) =
240 val _ = trace "crule_to_frule: cl'" (fn () => printVal cl')
242 (sub, FACT (cl', susp_map vf th))
245 val cls' = crule cl
247 trace "crule_to_frule: ((cl, th), cls')"
248 (fn () => printVal ((cl, th), cls'))
460 fn cl as CLAUSE (vars, lits) =>
465 val cl' = CLAUSE (vars, rev lits')
466 val _ = trace "lconv_to_cconv: (cl, cl')" (fn () => printVal (cl, cl'))
467 val res = [(empty_subst, cl', rule')]