TFL/tfl.ML

       | S.LAMB _ => raise TFL_ERR "FV_multiset" "lambda";
 
 fun no_repeat_vars thy pat =
  let fun check [] = true
        | check (v::rst) =
-         if mem_term (v,rst) then
+         if member (op aconv) rst v then
             raise TFL_ERR "no_repeat_vars"
                           (quote (#1 (dest_Free v)) ^
                           " occurs repeatedly in the pattern " ^
                           quote (string_of_cterm (Thry.typecheck thy pat)))
          else check rst

      val dummy = map (no_repeat_vars thy) pats
      val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
                               map (fn (t,i) => (t,(i,true))) (enumerate R))
      val names = foldr add_term_names [] R
      val atype = type_of(hd pats)
-     and aname = variant names "a"
+     and aname = Name.variant names "a"
      val a = Free(aname,atype)
      val ty_info = Thry.match_info thy
      val ty_match = Thry.match_type thy
      val range_ty = type_of (hd R)
      val (patts, case_tm) = mk_case ty_info ty_match (aname::names) range_ty

                  else ()
      val (case_rewrites,context_congs) = extraction_thms thy
      val tych = Thry.typecheck thy
      val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
      val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
-     val R = Free (variant (foldr add_term_names [] eqns) Rname,
+     val R = Free (Name.variant (foldr add_term_names [] eqns) Rname,
                    Rtype)
      val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
      val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
      val dummy =
            if !trace then

  let val tych = Thry.typecheck thy
      val ty_info = Thry.induct_info thy
  in fn pats =>
  let val names = foldr add_term_names [] pats
      val T = type_of (hd pats)
-     val aname = Term.variant names "a"
-     val vname = Term.variant (aname::names) "v"
+     val aname = Name.variant names "a"
+     val vname = Name.variant (aname::names) "v"
      val a = Free (aname, T)
      val v = Free (vname, T)
      val a_eq_v = HOLogic.mk_eq(a,v)
      val ex_th0 = R.EXISTS (tych (S.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
                            (R.REFL (tych a))

 let val tych = Thry.typecheck thy
     val Sinduction = R.UNDISCH (R.ISPEC (tych R) Thms.WF_INDUCTION_THM)
     val (pats,TCsl) = ListPair.unzip pat_TCs_list
     val case_thm = complete_cases thy pats
     val domain = (type_of o hd) pats
-    val Pname = Term.variant (foldr (Library.foldr add_term_names)
+    val Pname = Name.variant (foldr (Library.foldr add_term_names)
                               [] (pats::TCsl)) "P"
     val P = Free(Pname, domain --> HOLogic.boolT)
     val Sinduct = R.SPEC (tych P) Sinduction
     val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct)
     val Rassums_TCl' = map (build_ih fconst (P,SV)) pat_TCs_list
     val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
     val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums))
     val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
     val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
     val proved_cases = map (prove_case fconst thy) tasks
-    val v = Free (variant (foldr add_term_names [] (map concl proved_cases))
+    val v = Free (Name.variant (foldr add_term_names [] (map concl proved_cases))
                     "v",
                   domain)
     val vtyped = tych v
     val substs = map (R.SYM o R.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
     val proved_cases1 = ListPair.map (fn (th,th') => R.SUBS[th]th')