# HG changeset patch
# User haftmann
# Date 1648409270 0
# Node ID 96c19d03b5a576789af86c4f34bcb7115c18af5d
# Parent  48922e5656277cdb8bba3834a0f4a54b218c385b
tuned whitespace

diff -r 48922e565627 -r 96c19d03b5a5 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Fri Mar 25 17:21:39 2022 +0100
+++ b/src/Tools/Code/code_thingol.ML	Sun Mar 27 19:27:50 2022 +0000
@@ -279,11 +279,13 @@
         clauses = (map o apply2) (map_terms_bottom_up f) clauses,
         primitive = map_terms_bottom_up f t0 });
 
-fun adjungate_clause ctxt vs_map ts (body as IConst { sym = Constant c, ... }) =
+fun adjungate_clause ctxt vs_map ts
+    (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 (body as ICase { term = IVar (SOME v), clauses = clauses, ... }) =
+  | adjungate_clause ctxt vs_map ts
+    (body as ICase { term = IVar (SOME v), clauses = clauses, ... }) =
       let
         val vs = (fold o fold_varnames) (insert (op =)) ts [];
         fun varnames_disjunctive pat =
@@ -300,9 +302,9 @@
           orelse not (exists_var body' v)) clauses
           andalso forall (varnames_disjunctive o fst) clauses
         then case AList.lookup (op =) vs_map v
-         of SOME i => maps (fn (pat', body') =>
+         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') clauses
+                (nth_map i (K pat') ts |> map (purge_unused_vars_in body')) body')
           | NONE => [(ts, body)]
         else [(ts, body)]
       end
@@ -734,14 +736,17 @@
     fun distill_clause tys t =
       let
         val (vs, body) = unfold_abs_eta tys t;
-        val vs_map = fold_index (fn (i, (SOME v, _)) => cons (v, i) | _ => I) vs [];
+        val vs_map =
+          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;
     fun mk_clauses [] ty (t, ts_clause) =
-          (t, map (fn ([t], body) => (t, body)) (distill_clause [ty] (the_single ts_clause)))
+          (t, map (fn ([t], body) => (t, body))
+            (distill_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 (ts, body) => (constr `$$ ts, body))
+              (distill_clause (take n tys) t))
               (constrs ~~ ts_clause));
   in
     translate_const ctxt algbr eqngr permissive some_thm (c_ty, NONE)