# HG changeset patch
# User haftmann
# Date 1449481748 -3600
# Node ID 5daa82ba4078c7720df7ded3f627ead14a4da8bd
# Parent  a16497c686cbddb781053f18d808ba48fb992b14
clarified terminology

diff -r a16497c686cb -r 5daa82ba4078 NEWS
--- a/NEWS	Wed Dec 09 21:20:56 2015 +0100
+++ b/NEWS	Mon Dec 07 10:49:08 2015 +0100
@@ -346,12 +346,12 @@
     notation right.derived ("\<odot>''")
   end
 
-* Command 'sublocale' accepts mixin definitions after keyword
+* Command 'sublocale' accepts rewrite definitions after keyword
 'defines'.
 
 * Command 'permanent_interpretation' is available in Pure, without
 need to load a separate theory.  Keyword 'defines' identifies
-mixin definitions, keyword 'rewrites' identifies rewrite morphisms.
+rewrite definitions, keyword 'rewrites' identifies rewrite equations.
 INCOMPATIBILITY.
 
 * Command 'print_definitions' prints dependencies of definitional
diff -r a16497c686cb -r 5daa82ba4078 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Wed Dec 09 21:20:56 2015 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Mon Dec 07 10:49:08 2015 +0100
@@ -670,7 +670,9 @@
   proved explicitly the user. Such rewrite definitions are a even more useful
   device for interpreting concepts introduced through definitions, but they
   are only supported for interpretation commands operating in a local theory
-  whose implementing target actually supports this.
+  whose implementing target actually supports this.  Note that despite
+  the suggestive \<^theory_text>\<open>and\<close> connective, \<open>defs\<close>
+  are parsed sequentially without mutual recursion.
 
   \<^descr> \<^theory_text>\<open>interpretation expr rewrites eqns\<close> interprets \<open>expr\<close> into a local theory
   such that its lifetime is limited to the current context block (e.g. a
@@ -773,6 +775,13 @@
   \end{warn}
 
   \begin{warn}
+    Due to a technical limitation, the specific context of a interpretation
+    given by a \<^theory_text>\<open>for\<close> clause can get lost between a \<^theory_text>\<open>defines\<close> and
+    \<^theory_text>\<open>rewrites\<close> clause and must then be recovered manually using
+    explicit sort constraints and quantified term variables.
+  \end{warn}
+
+  \begin{warn}
     While \<^theory_text>\<open>interpretation (in c) \<dots>\<close> is admissible, it is not useful since
     its result is discarded immediately.
   \end{warn}
diff -r a16497c686cb -r 5daa82ba4078 src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Wed Dec 09 21:20:56 2015 +0100
+++ b/src/Pure/Isar/interpretation.ML	Mon Dec 07 10:49:08 2015 +0100
@@ -177,7 +177,7 @@
 end;
 
 
-(* algebraic-view *)
+(* algebraic view *)
 
 local