merged

--- a/src/Pure/Isar/code.ML	Tue May 02 15:17:39 2023 +0100
+++ b/src/Pure/Isar/code.ML	Wed May 03 10:35:20 2023 +0100
@@ -758,29 +758,24 @@
 
 fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (Proof_Context.init_global thy);
 
-fun expand_eta thy k thm =
-  let
-    val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
-    val (_, args) = strip_comb lhs;
-    val l = if k = ~1
-      then (length o fst o strip_abs) rhs
-      else Int.max (0, k - length args);
-    val (raw_vars, _) = Term.strip_abs_eta l rhs;
-    val vars = burrow_fst (Name.variant_list (map (fst o fst) (Term.add_vars lhs [])))
-      raw_vars;
-    fun expand (v, ty) thm = Drule.fun_cong_rule thm
-      (Thm.global_cterm_of thy (Var ((v, 0), ty)));
-  in
-    thm
-    |> fold expand vars
-    |> Conv.fconv_rule Drule.beta_eta_conversion
-  end;
-
 fun same_arity thy thms =
   let
-    val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
-    val k = fold (Integer.max o num_args_of o Thm.prop_of) thms 0;
-  in map (expand_eta thy k) thms end;
+    val lhs_rhss = map (Logic.dest_equals o Thm.plain_prop_of) thms;
+    val k = fold (Integer.max o length o snd o strip_comb o fst) lhs_rhss 0;
+    fun expand_eta (lhs, rhs) thm =
+      let
+        val l = k - length (snd (strip_comb lhs));
+        val (raw_vars, _) = Term.strip_abs_eta l rhs;
+        val vars = burrow_fst (Name.variant_list (map (fst o fst) (Term.add_vars lhs [])))
+          raw_vars;
+        fun expand (v, ty) thm = Drule.fun_cong_rule thm
+          (Thm.global_cterm_of thy (Var ((v, 0), ty)));
+      in
+        thm
+        |> fold expand vars
+        |> Conv.fconv_rule Drule.beta_eta_conversion
+      end;
+  in map2 expand_eta lhs_rhss thms end;
 
 fun mk_desymbolization pre post mk vs =
   let

--- a/src/Tools/Code/code_thingol.ML	Tue May 02 15:17:39 2023 +0100
+++ b/src/Tools/Code/code_thingol.ML	Wed May 03 10:35:20 2023 +0100
@@ -732,20 +732,17 @@
         then translation_error ctxt permissive some_thm deps
           "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
       else ()
-  in translate_const_proper ctxt algbr eqngr permissive some_thm (c, ty) (deps, program) end
-and translate_const_proper ctxt algbr eqngr permissive some_thm (c, ty) =
-  let
-    val thy = Proof_Context.theory_of ctxt;
     val (annotate, ty') = dest_tagged_type ty;
     val typargs = Sign.const_typargs thy (c, ty');
     val sorts = Code_Preproc.sortargs eqngr c;
     val (dom, range) = Term.strip_type ty';
   in
-    ensure_const ctxt algbr eqngr permissive c
-    ##>> fold_map (translate_typ ctxt algbr eqngr permissive) typargs
-    ##>> fold_map (translate_dicts ctxt algbr eqngr permissive some_thm) (typargs ~~ sorts)
-    ##>> fold_map (translate_typ ctxt algbr eqngr permissive) (range :: dom)
-    #>> (fn (((c, typargs), dss), range :: dom) =>
+    (deps, program)
+    |> ensure_const ctxt algbr eqngr permissive c
+    ||>> fold_map (translate_typ ctxt algbr eqngr permissive) typargs
+    ||>> fold_map (translate_dicts ctxt algbr eqngr permissive some_thm) (typargs ~~ sorts)
+    ||>> fold_map (translate_typ ctxt algbr eqngr permissive) (range :: dom)
+    |>> (fn (((c, typargs), dss), range :: dom) =>
       { sym = Constant c, typargs = typargs, dicts = dss,
         dom = dom, range = range, annotation =
           if annotate then SOME (dom `--> range) else NONE })
@@ -770,7 +767,7 @@
           |> nth_drop t_pos
           |> curry (op ~~) case_pats
           |> map_filter (fn (NONE, _) => NONE | (SOME _, x) => SOME x);
-        val tys = take (length case_pats + 1) (binder_types (snd (dest_tagged_type ty)));
+        val tys = take (length case_pats + 1) (binder_types ty);
         val ty_case = project_term tys;
         val ty_case' = project_term dom;
         val constrs = map_filter I case_pats ~~ project_cases tys
@@ -789,20 +786,20 @@
               clauses = (filter_out (is_undefined_clause ctxt) o distill_clauses constrs o project_cases) ts,
               primitive = IConst const `$$ ts })
       end
-and translate_app_case ctxt algbr eqngr permissive some_thm pattern_schema ty const ((vs_tys, (ts1, rty)), ts2) =
-  translate_case ctxt algbr eqngr permissive some_thm pattern_schema ty (const, ts1)
-  #>> (fn t => (vs_tys `|==> (t, rty)) `$$ ts2)
 and translate_app ctxt algbr eqngr permissive some_thm some_abs (c_ty as (c, ty), ts) =
-  case Code.get_case_schema (Proof_Context.theory_of ctxt) c of
-    SOME (wanted, pattern_schema) =>
-      translate_const ctxt algbr eqngr permissive some_thm some_abs c_ty
-      ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm NONE) ts
-      #-> (fn (const, ts) => translate_app_case ctxt algbr eqngr permissive some_thm pattern_schema
-            ty const (satisfied_application wanted (const, ts)))
-  | NONE =>
-      translate_const ctxt algbr eqngr permissive some_thm some_abs c_ty
-      ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm NONE) ts
-      #>> (fn (const, ts) => IConst const `$$ ts)
+  translate_const ctxt algbr eqngr permissive some_thm some_abs c_ty
+  ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm NONE) ts
+  #-> (fn (const, ts) => case Code.get_case_schema (Proof_Context.theory_of ctxt) c of
+      SOME (wanted, pattern_schema) =>
+        let
+          val ((vs_tys, (ts1, rty)), ts2) = satisfied_application wanted (const, ts);
+          val (_, ty') = dest_tagged_type ty;
+        in
+          translate_case ctxt algbr eqngr permissive some_thm pattern_schema ty' (const, ts1)
+          #>> (fn t => (vs_tys `|==> (t, rty)) `$$ ts2)
+        end
+    | NONE =>
+        pair (IConst const `$$ ts))
 and translate_tyvar_sort ctxt (algbr as (proj_sort, _)) eqngr permissive (v, sort) =
   fold_map (ensure_class ctxt algbr eqngr permissive) (proj_sort sort)
   #>> (fn sort => (unprefix "'" v, sort))