# HG changeset patch
# User haftmann
# Date 1648472053 0
# Node ID 75c69cbffe5f73659463b98d317c407ee2238546
# Parent  9257e7732766fb5dedca0da4778c19004c45420d
separated treatment of undefined bodys

diff -r 9257e7732766 -r 75c69cbffe5f src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Mar 28 12:54:11 2022 +0000
+++ b/src/Tools/Code/code_thingol.ML	Mon Mar 28 12:54:13 2022 +0000
@@ -284,14 +284,9 @@
         clauses = (map o apply2) (map_terms_bottom_up f) clauses,
         primitive = map_terms_bottom_up f t0 });
 
-fun distill_minimized_clause ctxt tys t =
+fun distill_minimized_clause tys t =
   let
     fun distill vs_map pat_args
-        (body as IConst { sym = Constant c, ... }) =
-          if Code.is_undefined (Proof_Context.theory_of ctxt) c
-          then []
-          else [(pat_args, body)]
-      | distill vs_map pat_args
         (body as ICase { term = IVar (SOME v), clauses = clauses, ... }) =
           let
             val vs = build (fold add_varnames pat_args);
@@ -745,14 +740,21 @@
   let
     val (ty, constrs, split_clauses) =
       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)))
-      | mk_clauses constrs ty (t, ts_clause) =
-          (t, maps (fn ((constr as IConst { dom = tys, ... }, n), t) =>
+    fun is_undefined_clause (_, IConst { sym = Constant c, ... }) =
+          Code.is_undefined (Proof_Context.theory_of ctxt) c
+      | is_undefined_clause _ =
+          false;
+    fun distill_clauses constrs ty ts =
+      let
+        val (t, ts_clause) = split_clauses ts;
+        val clauses = if null constrs
+          then map (fn ([pat], body) => (pat, body))
+            (distill_minimized_clause [ty] (the_single ts_clause))
+          else maps (fn ((constr as IConst { dom = tys, ... }, n), t) =>
             map (fn (pat_args, body) => (constr `$$ pat_args, body))
-              (distill_minimized_clause ctxt (take n tys) t))
-              (constrs ~~ ts_clause));
+              (distill_minimized_clause (take n tys) t))
+              (constrs ~~ ts_clause);
+      in (t, filter_out is_undefined_clause clauses) end;
   in
     translate_const ctxt algbr eqngr permissive some_thm (c_ty, NONE)
     ##>> fold_map (fn (constr, n) => translate_const ctxt algbr eqngr permissive some_thm (constr, NONE)
@@ -760,7 +762,7 @@
     ##>> translate_typ ctxt algbr eqngr permissive ty
     ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts
     #>> (fn (((t_app, constrs), ty), ts) =>
-      case mk_clauses constrs ty (split_clauses ts) of (t, clauses) =>
+      case distill_clauses constrs ty ts of (t, clauses) =>
         ICase { term = t, typ = ty, clauses = clauses, primitive = t_app `$$ ts })
   end
 and translate_app_case ctxt algbr eqngr permissive some_thm (num_args, pattern_schema) ((c, ty), ts) =