Lines Matching defs:cs
354 val cs =
361 val tm1 = Term.subst (List.map (op |->) (ListPair.zip (vs, cs))) tm1
366 val tys = List.map Term.type_of cs
368 val l = Term.list_mk_comb (Term.mk_var (s, ty), cs @ [d])
420 val (cs, defs) = ListPair.unzip l
421 val proj_r = TypeBase.mk_pattern_fn cs
979 val (cs, ps) = List.partition progSyntax.is_cond ts
980 val cs = List.map progSyntax.dest_cond cs
996 (fn t => List.map (fn c => d_rule o move_match (c, t)) cs)
1065 fun mk_frame cs = Term.mk_comb (Term.mk_comb (m_tm, df_intro cs), f)
1102 val (cs, ds) = ListPair.unzip cs_ds
1103 val frame = mk_frame cs
1645 val (cs, vs) = List.partition no_free rs
1647 (cs @ vs)