# HG changeset patch
# User haftmann
# Date 1648139681 0
# Node ID a82f7f8a3c7bf5e7253eb365494053c0a8297074
# Parent  b7a74a04ae4e2d41c9aefc3b942dfa4ea28a97f2
self-contained extraction auf clauses

diff -r b7a74a04ae4e -r a82f7f8a3c7b src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu Mar 24 16:34:40 2022 +0000
+++ b/src/Tools/Code/code_thingol.ML	Thu Mar 24 16:34:41 2022 +0000
@@ -678,18 +678,21 @@
     val thy = Proof_Context.theory_of ctxt;
     val ty = nth (binder_types (snd c_ty)) t_pos;
     val is_let = null case_pats;
-    fun mk_constr NONE _ = NONE
-      | mk_constr (SOME c) t =
-          let
-            val n = Code.args_number thy c;
-          in SOME ((c, (take n o binder_types o fastype_of o untag_term) t ---> ty), n) end;
+    fun select_clauses xs =
+      xs
+      |> nth_drop t_pos
+      |> curry (op ~~) case_pats
+      |> map_filter (fn (NONE, _) => NONE | (SOME _, x) => SOME x);
+    fun mk_constr c t =
+      let
+        val n = Code.args_number thy c;
+      in ((c, (take n o binder_types o fastype_of o untag_term) t ---> ty), n) end;
     val constrs =
       if is_let then []
-      else map_filter I (map2 mk_constr case_pats (nth_drop t_pos ts));
+      else map2 mk_constr (case_pats |> map_filter I) (select_clauses ts);
     val split_clauses =
       if is_let then (fn ts => (nth ts t_pos, nth_drop t_pos ts))
-        else (fn ts => (nth ts t_pos, ts |> nth_drop t_pos |> curry (op ~~) case_pats
-          |> map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t)));
+        else (fn ts => (nth ts t_pos, select_clauses ts));
     fun disjunctive_varnames ts =
       let
         val vs = (fold o fold_varnames) (insert (op =)) ts [];