# HG changeset patch
# User haftmann
# Date 1648409273 0
# Node ID cbefaa400da28dac6cae4eedfc433a9fa0422380
# Parent  05f7f5454cb6bd40e0490ff2c3e6b7f0024e33d2
tuned names

diff -r 05f7f5454cb6 -r cbefaa400da2 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sun Mar 27 19:27:52 2022 +0000
+++ b/src/Tools/Code/code_thingol.ML	Sun Mar 27 19:27:53 2022 +0000
@@ -279,15 +279,15 @@
         clauses = (map o apply2) (map_terms_bottom_up f) clauses,
         primitive = map_terms_bottom_up f t0 });
 
-fun adjungate_clause ctxt vs_map ts
+fun distill_minimized_clause' ctxt vs_map pat_args
     (body as IConst { sym = Constant c, ... }) =
       if Code.is_undefined (Proof_Context.theory_of ctxt) c
       then []
-      else [(ts, body)]
-  | adjungate_clause ctxt vs_map ts
+      else [(pat_args, body)]
+  | distill_minimized_clause' ctxt vs_map pat_args
     (body as ICase { term = IVar (SOME v), clauses = clauses, ... }) =
       let
-        val vs = build ((fold o fold_varnames) (insert (op =)) ts);
+        val vs = build ((fold o fold_varnames) (insert (op =)) pat_args);
         fun varnames_disjunctive pat =
           null (inter (op =) vs (build (fold_varnames (insert (op =)) pat)));
         fun purge_unused_vars_in t =
@@ -303,12 +303,12 @@
           andalso forall (varnames_disjunctive o fst) clauses
         then case AList.lookup (op =) vs_map v
          of SOME i => clauses |> maps (fn (pat', body') =>
-              adjungate_clause ctxt (AList.delete (op =) v vs_map)
-                (nth_map i (K pat') ts |> map (purge_unused_vars_in body')) body')
-          | NONE => [(ts, body)]
-        else [(ts, body)]
+              distill_minimized_clause' ctxt (AList.delete (op =) v vs_map)
+                (nth_map i (K pat') pat_args |> map (purge_unused_vars_in body')) body')
+          | NONE => [(pat_args, body)]
+        else [(pat_args, body)]
       end
-  | adjungate_clause ctxt vs_map ts body = [(ts, body)];
+  | distill_minimized_clause' ctxt vs_map pat_args body = [(pat_args, body)];
 
 fun exists_dict_var f (Dict (_, d)) = exists_plain_dict_var_pred f d
 and exists_plain_dict_var_pred f (Dict_Const (_, dss)) = exists_dictss_var f dss
@@ -733,20 +733,20 @@
   let
     val (ty, constrs, split_clauses) =
       preprocess_pattern_schema ctxt (t_pos, case_pats) (c_ty, ts);
-    fun distill_clause tys t =
+    fun distill_minimized_clause tys t =
       let
         val (vs, body) = unfold_abs_eta tys t;
         val vs_map =
           build (fold_index (fn (i, (SOME v, _)) => cons (v, i) | _ => I) vs);
-        val ts = map (IVar o fst) vs;
-      in adjungate_clause ctxt vs_map ts body end;
+        val pat_args = map (IVar o fst) vs;
+      in distill_minimized_clause' ctxt vs_map pat_args body end;
     fun mk_clauses [] ty (t, ts_clause) =
-          (t, map (fn ([t], body) => (t, body))
-            (distill_clause [ty] (the_single ts_clause)))
+          (t, map (fn ([pat], body) => (pat, body))
+            (distill_minimized_clause [ty] (the_single ts_clause)))
       | mk_clauses constrs ty (t, ts_clause) =
           (t, maps (fn ((constr as IConst { dom = tys, ... }, n), t) =>
-            map (fn (ts, body) => (constr `$$ ts, body))
-              (distill_clause (take n tys) t))
+            map (fn (pat_args, body) => (constr `$$ pat_args, body))
+              (distill_minimized_clause (take n tys) t))
               (constrs ~~ ts_clause));
   in
     translate_const ctxt algbr eqngr permissive some_thm (c_ty, NONE)