# HG changeset patch
# User haftmann
# Date 1648139678 0
# Node ID fd3d66066256ebdc96126c60ea27c537ce172e09
# Parent  c7ff16398535adf21764ca17bf57be8984692d2c
streamlined

diff -r c7ff16398535 -r fd3d66066256 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu Mar 24 16:34:37 2022 +0000
+++ b/src/Tools/Code/code_thingol.ML	Thu Mar 24 16:34:38 2022 +0000
@@ -721,13 +721,13 @@
     fun casify constrs ty t_app ts =
       let
         val t = nth ts t_pos;
-        val ts_clause = nth_drop t_pos ts;
+        val ts_clause = ts |> nth_drop t_pos |> curry (op ~~) case_pats
+          |> map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t);
         val clauses = if null case_pats
           then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
           else maps (fn ((constr as IConst { dom = tys, ... }, n), t) =>
             mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
-              (constrs ~~ (map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t)
-                (case_pats ~~ ts_clause)));
+              (constrs ~~ ts_clause);
       in ICase { term = t, typ = ty, clauses = clauses, primitive = t_app `$$ ts } end;
   in
     translate_const ctxt algbr eqngr permissive some_thm (c_ty, NONE)