TFL/tfl.sml

  *---------------------------------------------------------------------------*)
 fun mk_group Name rows =
   U.itlist (fn (row as ((prfx, p::rst), rhs)) =>
             fn (in_group,not_in_group) =>
                let val (pc,args) = S.strip_comb p
-               in if ((#1(dest_Const pc) = Name) handle _ => false)
+               in if ((#1(dest_Const pc) = Name) handle _ => false) (* FIXME do not handle _ !!! *)
                   then (((prfx,args@rst), rhs)::in_group, not_in_group)
                   else (in_group, row::not_in_group) end)
       rows ([],[]);
 
 (*---------------------------------------------------------------------------

                    (Int.toString (length fs) ^
                     " distinct function names being declared")
 in
 fun mk_functional thy clauses =
  let val (L,R) = ListPair.unzip (map HOLogic.dest_eq clauses)
-                   handle _ => raise TFL_ERR
+                   handle _ => raise TFL_ERR (* FIXME do not handle _ !!! *)
                        {func = "mk_functional",
                         mesg = "recursion equations must use the = relation"}
      val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
      val atom = single (gen_distinct (op aconv) funcs)
      val (fname,ftype) = dest_atom atom

      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
                                     {path=[a], rows=rows}
      val patts1 = map (fn (_,tag,[pat]) => (pat,tag)) patts
-          handle _ => mk_functional_err "error in pattern-match translation"
+          handle _ => mk_functional_err "error in pattern-match translation" (* FIXME do not handle _ !!! *)
      val patts2 = U.sort(fn p1=>fn p2=> row_of_pat p1 < row_of_pat p2) patts1
      val finals = map row_of_pat patts2
      val originals = map (row_of_pat o #2) rows
      val dummy = case (originals\\finals)
              of [] => ()

          in case cntxt
               of [] => (P_y, (tm,[]))
                | _  => let
                     val imp = S.list_mk_conj cntxt ==> P_y
                     val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals)
-                    val locals = #2(U.pluck (curry (op aconv) P) lvs) handle _ => lvs
+                    val locals = #2(U.pluck (curry (op aconv) P) lvs) handle _ => lvs (* FIXME do not handle _ !!! *)
                     in (S.list_mk_forall(locals,imp), (tm,locals)) end
          end
  in case TCs
     of [] => (S.list_mk_forall(globals, P$pat), [])
      |  _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)

          in case cntxt
               of [] => (P_y, (tm,[]))
                | _  => let
                     val imp = S.list_mk_conj cntxt ==> P_y
                     val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals)
-                    val locals = #2(U.pluck (curry (op aconv) P) lvs) handle _ => lvs
+                    val locals = #2(U.pluck (curry (op aconv) P) lvs) handle _ => lvs (* FIXME do not handle _ !!! *)
                     in (S.list_mk_forall(locals,imp), (tm,locals)) end
          end
  in case TCs
     of [] => (S.list_mk_forall(pat_vars, P$pat), [])
      |  _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)

      fun nested tm = is_some (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 _ => th2
+              then R.DISCH (get_cntxt TC) th2 handle _ => th2 (* FIXME do not handle _ !!! *)
                else if S.is_imp(concl TC)
                      then R.IMP_TRANS TC th2
                       else R.MP th2 TC)
  in
  R.DISCH antc

     val dc' = U.itlist (R.GEN o tych) vars
                        (R.SPEC (tych(S.mk_vstruct Parg_ty vars)) dc)
 in
    R.GEN (tych P) (R.DISCH (tych(concl Rinduct_assum)) dc')
 end
-handle _ => raise TFL_ERR{func = "mk_induction", mesg = "failed derivation"};
+handle _ => raise TFL_ERR{func = "mk_induction", mesg = "failed derivation"}; (* FIXME do not handle _ !!! *)
 
 
 
 
 (*---------------------------------------------------------------------------

    val (rules1,induction1)  =
        let val thm = R.prove(tych(HOLogic.mk_Trueprop
                                   (hd(#1(R.dest_thm rules)))),
                              wf_tac)
        in (R.PROVE_HYP thm rules,  R.PROVE_HYP thm induction)
-       end handle _ => (rules,induction)
+       end handle _ => (rules,induction) (* FIXME do not handle _ !!! *)
 
    (*----------------------------------------------------------------------
     * The termination condition (tc) is simplified to |- tc = tc' (there
     * might not be a change!) and then 3 attempts are made:
     *

            val _ = print_cterms "TC before simplification: " [tc1]
            val tc_eq = simplifier tc1
            val _ = print_thms "result: " [tc_eq]
        in
        elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
-       handle _ =>
+       handle _ => (* FIXME do not handle _ !!! *)
         (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
                   (R.prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))),
                            terminator)))
                  (r,ind)
-         handle _ =>
+         handle _ => (* FIXME do not handle _ !!! *)
           (R.UNDISCH(R.MATCH_MP (R.MATCH_MP Thms.simp_thm r) tc_eq),
            simplify_induction theory tc_eq ind))
        end
 
    (*----------------------------------------------------------------------

    fun simplify_nested_tc tc =
       let val tc_eq = simplifier (tych (#2 (S.strip_forall tc)))
       in
       R.GEN_ALL
        (R.MATCH_MP Thms.eqT tc_eq
-        handle _
+        handle _ (* FIXME do not handle _ !!! *)
         => (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
                       (R.prove(tych(HOLogic.mk_Trueprop (S.rhs(concl tc_eq))),
                                terminator))
-            handle _ => tc_eq))
+            handle _ => tc_eq)) (* FIXME do not handle _ !!! *)
       end
 
    (*-------------------------------------------------------------------
     * Attempt to simplify the termination conditions in each rule and
     * in the induction theorem.