--- 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;