src/Tools/permanent_interpretation.ML

 
     (*defining*)
     val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
       ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
     val (defs, defs_ctxt) = fold_map Local_Theory.define pre_defs expr_ctxt1;
-    val def_eqns = map (Thm.symmetric o Morphism.thm (Local_Theory.standard_morphism defs_ctxt expr_ctxt1) o snd o snd) defs;
     val expr_ctxt2 = Proof_Context.transfer (Proof_Context.theory_of defs_ctxt) expr_ctxt1;
+    val def_eqns = defs
+      |> map (Thm.symmetric o
+        Morphism.thm (Local_Theory.standard_morphism defs_ctxt expr_ctxt2) o snd o snd);
 
     (*setting up*)
     val attrss = map (apsnd (map (prep_attr expr_ctxt2)) o fst) raw_eqns;
     val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt2;
     val export' = Variable.export_morphism goal_ctxt expr_ctxt2;