# HG changeset patch
# User haftmann
# Date 1449080097 -3600
# Node ID 2256ef8224f6078b34d8c8b351e2f7cdddde7005
# Parent  2f33f6cc964d6a709bf1668ad00b179bce3d12ea
clarified role of context for reading rewrite specifications

diff -r 2f33f6cc964d -r 2256ef8224f6 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)