TFL/tfl.ML

  *---------------------------------------------------------------------------*)
 
 fun mk_pat (c,l) =
   let val L = length (binder_types (type_of c))
       fun build (prfx,tag,plist) =
-          let val args   = take (L,plist)
-              and plist' = drop(L,plist)
+          let val args   = Library.take (L,plist)
+              and plist' = Library.drop(L,plist)
           in (prfx,tag,list_comb(c,args)::plist') end
   in map build l end;
 
 fun v_to_prfx (prfx, v::pats) = (v::prfx,pats)
   | v_to_prfx _ = raise TFL_ERR "mk_case" "v_to_prfx";

      val atom = single (gen_distinct (op aconv) funcs)
      val (fname,ftype) = dest_atom atom
      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 names = Library.foldr add_term_names (R,[])
      val atype = type_of(hd pats)
      and aname = variant names "a"
      val a = Free(aname,atype)
      val ty_info = Thry.match_info thy
      val ty_match = Thry.match_type thy

 in
   pass (TCs, map (fn p => (p,[])) full_pats)
 end;
 
 
-fun givens pats = map pat_of (filter given pats);
+fun givens pats = map pat_of (List.filter given pats);
 
 fun post_definition meta_tflCongs (theory, (def, pats)) =
  let val tych = Thry.typecheck theory
      val f = #lhs(S.dest_eq(concl def))
      val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def
-     val pats' = filter given pats
+     val pats' = List.filter given pats
      val given_pats = map pat_of pats'
      val rows = map row_of_pat pats'
      val WFR = #ant(S.dest_imp(concl corollary))
      val R = #Rand(S.dest_comb WFR)
      val corollary' = R.UNDISCH corollary  (* put WF R on assums *)

                  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 (variant (Library.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

      val dummy = if !trace
                  then (writeln "Extractants = ";
                        prths extractants;
                        ())
                  else ()
-     val TCs = foldr (gen_union (op aconv)) (TCl, [])
+     val TCs = Library.foldr (gen_union (op aconv)) (TCl, [])
      val full_rqt = WFR::TCs
      val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
      val R'abs = S.rand R'
      val proto_def' = subst_free[(R1,R')] proto_def
      val dummy = if !trace then writeln ("proto_def' = " ^

 
 fun alpha_ex_unroll (xlist, tm) =
   let val (qvars,body) = S.strip_exists tm
       val vlist = #2(S.strip_comb (S.rhs body))
       val plist = ListPair.zip (vlist, xlist)
-      val args = map (fn qv => the (gen_assoc (op aconv) (plist, qv))) qvars
+      val args = map (fn qv => valOf (gen_assoc (op aconv) (plist, qv))) qvars
                    handle Option => sys_error
                        "TFL fault [alpha_ex_unroll]: no correspondence"
       fun build ex      []   = []
         | build (_$rex) (v::rst) =
            let val ex1 = betapply(rex, v)

             fun expnd tm (pats,(th,b)) = (pats,(R.SUBS[R.ASSUME(tych tm)]th,b))
             val news = map (fn (nf,rows,c) => {path = nf@rstp,
                                                rows = map (expnd c) rows})
                            (U.zip3 new_formals groups constraints)
             val recursive_thms = map mk news
-            val build_exists = foldr
+            val build_exists = Library.foldr
                                 (fn((x,t), th) =>
                                  R.CHOOSE (tych x, R.ASSUME (tych t)) th)
             val thms' = ListPair.map build_exists (vexl, recursive_thms)
             val same_concls = R.EVEN_ORS thms'
         in R.DISJ_CASESL thm' same_concls

 
 fun complete_cases thy =
  let val tych = Thry.typecheck thy
      val ty_info = Thry.induct_info thy
  in fn pats =>
- let val names = foldr add_term_names (pats,[])
+ let val names = Library.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 a = Free (aname, T)
      val v = Free (vname, T)

 local infix 5 ==>
       fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
 in
 fun build_ih f P (pat,TCs) =
  let val globals = S.free_vars_lr pat
-     fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
+     fun nested tm = isSome (S.find_term (curry (op aconv) f) tm)
      fun dest_TC tm =
          let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
              val (R,y,_) = S.dest_relation R_y_pat
              val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
          in case cntxt

       fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
 in
 fun build_ih f (P,SV) (pat,TCs) =
  let val pat_vars = S.free_vars_lr pat
      val globals = pat_vars@SV
-     fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
+     fun nested tm = isSome (S.find_term (curry (op aconv) f) tm)
      fun dest_TC tm =
          let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
              val (R,y,_) = S.dest_relation R_y_pat
              val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
          in case cntxt

  *---------------------------------------------------------------------------*)
 fun prove_case f thy (tm,TCs_locals,thm) =
  let val tych = Thry.typecheck thy
      val antc = tych(#ant(S.dest_imp tm))
      val thm' = R.SPEC_ALL thm
-     fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
+     fun nested tm = isSome (S.find_term (curry (op aconv) f) tm)
      fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC)))))
      fun mk_ih ((TC,locals),th2,nested) =
          R.GENL (map tych locals)
             (if nested then R.DISCH (get_cntxt TC) th2 handle U.ERR _ => th2
              else if S.is_imp (concl TC) then R.IMP_TRANS TC th2

 fun LEFT_ABS_VSTRUCT tych thm =
   let fun CHOOSER v (tm,thm) =
         let val ex_tm = S.mk_exists{Bvar=v,Body=tm}
         in (ex_tm, R.CHOOSE(tych v, R.ASSUME (tych ex_tm)) thm)
         end
-      val [veq] = filter (can S.dest_eq) (#1 (R.dest_thm thm))
+      val [veq] = List.filter (can S.dest_eq) (#1 (R.dest_thm thm))
       val {lhs,rhs} = S.dest_eq veq
       val L = S.free_vars_lr rhs
   in  #2 (U.itlist CHOOSER L (veq,thm))  end;
 
 

 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 (foldr add_term_names)
+    val Pname = Term.variant (Library.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 => 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 (variant (Library.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')