# HG changeset patch # User haftmann # Date 1648472051 0 # Node ID 9257e7732766fb5dedca0da4778c19004c45420d # Parent fa014f31f208172358428bbf432da5993814c254 tuned arguments diff -r fa014f31f208 -r 9257e7732766 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Mon Mar 28 12:54:09 2022 +0000 +++ b/src/Tools/Code/code_thingol.ML Mon Mar 28 12:54:11 2022 +0000 @@ -741,10 +741,10 @@ translate_const ctxt algbr eqngr permissive some_thm (c_ty, some_abs) ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts #>> (fn (t, ts) => t `$$ ts) -and translate_case ctxt algbr eqngr permissive some_thm (t_pos, case_pats) (c_ty, ts) = +and translate_case ctxt algbr eqngr permissive some_thm pattern_schema (c_ty, ts) = let val (ty, constrs, split_clauses) = - preprocess_pattern_schema ctxt (t_pos, case_pats) (c_ty, ts); + preprocess_pattern_schema ctxt pattern_schema (c_ty, ts); fun mk_clauses [] ty (t, ts_clause) = (t, map (fn ([pat], body) => (pat, body)) (distill_minimized_clause ctxt [ty] (the_single ts_clause)))