# 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)))