Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
mixin definitions are within scope of "for"s of import expression
authorhaftmann
Wed, 11 Jun 2014 18:22:05 +0200
changeset 57224 2a7a789ed510
parent 57223 fe3f1ca1200a
child 57225 ff69e42ccf92
mixin definitions are within scope of "for"s of import expression
src/Tools/permanent_interpretation.ML file | annotate | diff | comparison | revisions 
--- a/src/Tools/permanent_interpretation.ML	Wed Jun 11 18:22:04 2014 +0200
+++ b/src/Tools/permanent_interpretation.ML	Wed Jun 11 18:22:05 2014 +0200
@@ -33,8 +33,8 @@
     (*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 initial_ctxt;
-    val def_eqns = map (Thm.symmetric o Morphism.thm (Local_Theory.standard_morphism defs_ctxt initial_ctxt) o snd o snd) defs;
+    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;
 
     (*setting up*)
isabelle