# HG changeset patch
# User haftmann
# Date 1641883667 0
# Node ID 1f30aa91f496e9e15c95d33babb19d251bdedbd2
# Parent  e4fd3989554d8cf10e8fad5bab228111fa0d2340
more correct transfer

diff -r e4fd3989554d -r 1f30aa91f496 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Jan 10 21:34:09 2022 +0100
+++ b/src/Pure/Isar/code.ML	Tue Jan 11 06:47:47 2022 +0000
@@ -1112,12 +1112,7 @@
 fun rewrite_eqn conv ctxt =
   singleton (Variable.trade (K (map (Conv.fconv_rule (conv (Simplifier.rewrite ctxt))))) ctxt)
 
-fun preprocess conv ctxt =
-  Thm.transfer' ctxt
-  #> rewrite_eqn conv ctxt
-  #> Axclass.unoverload ctxt;
-
-fun cert_of_eqns_preprocess ctxt functrans c =
+fun apply_functrans ctxt functrans =
   let
     fun trace_eqns s eqns = (Pretty.writeln o Pretty.chunks)
       (Pretty.str s :: map (Thm.pretty_thm ctxt o fst) eqns);
@@ -1126,19 +1121,25 @@
     tap (tracing "before function transformation")
     #> (perhaps o perhaps_loop o perhaps_apply) functrans
     #> tap (tracing "after function transformation")
-    #> (map o apfst) (preprocess eqn_conv ctxt)
-    #> cert_of_eqns ctxt c
   end;
 
+fun preprocess conv ctxt =
+  rewrite_eqn conv ctxt
+  #> Axclass.unoverload ctxt;
+
 fun get_cert ctxt functrans c =
   case lookup_proper_fun_spec (specs_of (Proof_Context.theory_of ctxt)) c of
     NONE => nothing_cert ctxt c
   | SOME (Eqns (_, eqns)) => eqns
-      |> cert_of_eqns_preprocess ctxt functrans c
+      |> (map o apfst) (Thm.transfer' ctxt)
+      |> apply_functrans ctxt functrans
+      |> (map o apfst) (preprocess eqn_conv ctxt)
+      |> cert_of_eqns ctxt c
   | SOME (Proj (_, (tyco, _))) => cert_of_proj ctxt c tyco
   | SOME (Abstr (abs_thm, (tyco, _))) => abs_thm
-     |> preprocess Conv.arg_conv ctxt
-     |> cert_of_abs ctxt tyco c;
+      |> Thm.transfer' ctxt
+      |> preprocess Conv.arg_conv ctxt
+      |> cert_of_abs ctxt tyco c;
 
 
 (* case certificates *)