# HG changeset patch
# User wenzelm
# Date 1444158708 -7200
# Node ID 201c21438177f1f4f60615b24d8e8e77dcec202d
# Parent  5b5656a63bd601736cea974e49a2e0d6a6b18804
proper context;

diff -r 5b5656a63bd6 -r 201c21438177 src/Tools/permanent_interpretation.ML
--- a/src/Tools/permanent_interpretation.ML	Tue Oct 06 17:47:28 2015 +0200
+++ b/src/Tools/permanent_interpretation.ML	Tue Oct 06 21:11:48 2015 +0200
@@ -34,8 +34,10 @@
     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;