tfl/src/Defn.sml

29 fun variants FV vlist =
33            let val v' = variant W v in (v'::V, v'::W) end) vlist ([],FV));
35 fun numvariants FV vlist =
39            let val v' = numvariant W v in (v'::V, v'::W) end) vlist ([],FV));
591      fun strings_of vlist =
593                                (Listsort.sort Term.compare vlist))
1059       val Vinj = map2 (fn f => fn vlist =>
1060                         beta_conv(mk_comb(#2 f, list_mk_pair vlist))) injmap V
1062       val tmpl = map (fn (vlist,v) =>
1063                          GENL vlist (Rules.simplify [sum_case_def]
1645  let val (vlist,body) = Absyn.strip_forall eq
1653                             ([],Lib.union V (map dest_pvar vlist))
1656      val new_eq       = Absyn.list_mk_forall(vlist, Absyn.mk_eq(new_lhs, rhs))