clarified role of context for reading rewrite specifications
authorhaftmann
Wed, 02 Dec 2015 19:14:57 +0100
changeset 61773 2256ef8224f6
parent 61772 2f33f6cc964d
child 61774 029162bc9793
clarified role of context for reading rewrite specifications
src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Wed Dec 02 19:14:56 2015 +0100
+++ b/src/Pure/Isar/interpretation.ML	Wed Dec 02 19:14:57 2015 +0100
@@ -52,13 +52,13 @@
 
 local
 
-fun prep_mixins prep_term prep_prop expr_ctxt deps_ctxt raw_defs raw_eqns =
+fun prep_mixins prep_term prep_prop expr_ctxt read_rew_ctxt raw_defs raw_eqns =
   let
-    val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt expr_ctxt;
-    val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs;
+    val prep = Syntax.check_terms read_rew_ctxt #> Variable.export_terms read_rew_ctxt expr_ctxt;
+    val rhss = (prep o map (prep_term read_rew_ctxt o snd o snd)) raw_defs;
     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 eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns;
+    val eqns = (prep o map (prep_prop read_rew_ctxt o snd)) raw_eqns;
   in (pre_defs, eqns) end;
 
 fun define_mixins [] expr_ctxt = ([], expr_ctxt)