# HG changeset patch
# User ballarin
# Date 1308997194 -7200
# Node ID eb8b4851b039ca4c1b4424d9624b6a4a1dcdc6fe
# Parent  de5c79682b569df3bed0c543969bd9ebeb0f0189
While reading equations of an interpretation, already allow syntax provided by the interpretation base.

diff -r de5c79682b56 -r eb8b4851b039 doc-src/Locales/Locales/Examples2.thy
--- a/doc-src/Locales/Locales/Examples2.thy	Thu Jun 23 23:12:00 2011 +0200
+++ b/doc-src/Locales/Locales/Examples2.thy	Sat Jun 25 12:19:54 2011 +0200
@@ -3,7 +3,7 @@
 begin
 text {* \vspace{-5ex} *}
   interpretation %visible int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool"
-    where "partial_order.less op \<le> (x::int) y = (x < y)"
+    where "int.less x y = (x < y)"
   proof -
     txt {* \normalsize The goals are now:
       @{subgoals [display]}
@@ -12,7 +12,7 @@
       by unfold_locales auto
     txt {* \normalsize The second goal is shown by unfolding the
       definition of @{term "partial_order.less"}. *}
-    show "partial_order.less op \<le> (x::int) y = (x < y)"
+    show "partial_order.less op \<le> x y = (x < y)"
       unfolding partial_order.less_def [OF `partial_order op \<le>`]
       by auto
   qed
diff -r de5c79682b56 -r eb8b4851b039 doc-src/Locales/Locales/Examples3.thy
--- a/doc-src/Locales/Locales/Examples3.thy	Thu Jun 23 23:12:00 2011 +0200
+++ b/doc-src/Locales/Locales/Examples3.thy	Sat Jun 25 12:19:54 2011 +0200
@@ -17,12 +17,12 @@
   repeat the example from the previous section to illustrate this. *}
 
   interpretation %visible int: partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
-    where "partial_order.less op \<le> (x::int) y = (x < y)"
+    where "int.less x y = (x < y)"
   proof -
     show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
       by unfold_locales auto
     then interpret int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool" .
-    show "partial_order.less op \<le> (x::int) y = (x < y)"
+    show "int.less x y = (x < y)"
       unfolding int.less_def by auto
   qed
 
@@ -47,8 +47,8 @@
   so they can be used in a later example.  *}
 
   interpretation %visible int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
-    where int_min_eq: "lattice.meet op \<le> (x::int) y = min x y"
-      and int_max_eq: "lattice.join op \<le> (x::int) y = max x y"
+    where int_min_eq: "int.meet x y = min x y"
+      and int_max_eq: "int.join x y = max x y"
   proof -
     show "lattice (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
       txt {* \normalsize We have already shown that this is a partial
@@ -69,9 +69,9 @@
       in a situation where the lattice theorems can be used in a
       convenient way. *}
     then interpret int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" .
-    show "lattice.meet op \<le> (x::int) y = min x y"
+    show "int.meet x y = min x y"
       by (bestsimp simp: int.meet_def int.is_inf_def)
-    show "lattice.join op \<le> (x::int) y = max x y"
+    show "int.join x y = max x y"
       by (bestsimp simp: int.join_def int.is_sup_def)
   qed
 
diff -r de5c79682b56 -r eb8b4851b039 doc-src/Locales/Locales/document/Examples2.tex
--- a/doc-src/Locales/Locales/document/Examples2.tex	Thu Jun 23 23:12:00 2011 +0200
+++ b/doc-src/Locales/Locales/document/Examples2.tex	Sat Jun 25 12:19:54 2011 +0200
@@ -30,7 +30,7 @@
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
 \ int{\isaliteral{3A}{\isacharcolon}}\ partial{\isaliteral{5F}{\isacharunderscore}}order\ {\isaliteral{22}{\isachardoublequoteopen}}op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5B}{\isacharbrackleft}}int{\isaliteral{2C}{\isacharcomma}}\ int{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}less\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3C}{\isacharless}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}int{\isaliteral{2E}{\isachardot}}less\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3C}{\isacharless}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \isacommand{proof}\isamarkupfalse%
 \ {\isaliteral{2D}{\isacharminus}}%
 \begin{isamarkuptxt}%
@@ -52,7 +52,7 @@
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}less\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3C}{\isacharless}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}less\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3C}{\isacharless}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
 \ partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}less{\isaliteral{5F}{\isacharunderscore}}def\ {\isaliteral{5B}{\isacharbrackleft}}OF\ {\isaliteral{60}{\isacharbackquoteopen}}partial{\isaliteral{5F}{\isacharunderscore}}order\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}{\isaliteral{60}{\isacharbackquoteclose}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
diff -r de5c79682b56 -r eb8b4851b039 doc-src/Locales/Locales/document/Examples3.tex
--- a/doc-src/Locales/Locales/document/Examples3.tex	Thu Jun 23 23:12:00 2011 +0200
+++ b/doc-src/Locales/Locales/document/Examples3.tex	Sat Jun 25 12:19:54 2011 +0200
@@ -49,7 +49,7 @@
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
 \ int{\isaliteral{3A}{\isacharcolon}}\ partial{\isaliteral{5F}{\isacharunderscore}}order\ {\isaliteral{22}{\isachardoublequoteopen}}op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}less\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3C}{\isacharless}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}int{\isaliteral{2E}{\isachardot}}less\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3C}{\isacharless}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \isacommand{proof}\isamarkupfalse%
 \ {\isaliteral{2D}{\isacharminus}}\isanewline
 \ \ \ \ \isacommand{show}\isamarkupfalse%
@@ -61,7 +61,7 @@
 \ int{\isaliteral{3A}{\isacharcolon}}\ partial{\isaliteral{5F}{\isacharunderscore}}order\ {\isaliteral{22}{\isachardoublequoteopen}}op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5B}{\isacharbrackleft}}int{\isaliteral{2C}{\isacharcomma}}\ int{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
 \isanewline
 \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}less\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3C}{\isacharless}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}int{\isaliteral{2E}{\isachardot}}less\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3C}{\isacharless}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
 \ int{\isaliteral{2E}{\isachardot}}less{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
 \ auto\isanewline
@@ -108,8 +108,8 @@
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
 \ int{\isaliteral{3A}{\isacharcolon}}\ lattice\ {\isaliteral{22}{\isachardoublequoteopen}}op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \isakeyword{where}\ int{\isaliteral{5F}{\isacharunderscore}}min{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}lattice{\isaliteral{2E}{\isachardot}}meet\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ min\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \ \ \isakeyword{and}\ int{\isaliteral{5F}{\isacharunderscore}}max{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}lattice{\isaliteral{2E}{\isachardot}}join\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ max\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \ \ \isakeyword{where}\ int{\isaliteral{5F}{\isacharunderscore}}min{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}int{\isaliteral{2E}{\isachardot}}meet\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ min\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \ \ \ \ \isakeyword{and}\ int{\isaliteral{5F}{\isacharunderscore}}max{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}int{\isaliteral{2E}{\isachardot}}join\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ max\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \isacommand{proof}\isamarkupfalse%
 \ {\isaliteral{2D}{\isacharminus}}\isanewline
 \ \ \ \ \isacommand{show}\isamarkupfalse%
@@ -157,11 +157,11 @@
 \ int{\isaliteral{3A}{\isacharcolon}}\ lattice\ {\isaliteral{22}{\isachardoublequoteopen}}op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
 \isanewline
 \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}lattice{\isaliteral{2E}{\isachardot}}meet\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ min\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}int{\isaliteral{2E}{\isachardot}}meet\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ min\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
 \ {\isaliteral{28}{\isacharparenleft}}bestsimp\ simp{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{2E}{\isachardot}}meet{\isaliteral{5F}{\isacharunderscore}}def\ int{\isaliteral{2E}{\isachardot}}is{\isaliteral{5F}{\isacharunderscore}}inf{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
 \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}lattice{\isaliteral{2E}{\isachardot}}join\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ max\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}int{\isaliteral{2E}{\isachardot}}join\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ max\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
 \ {\isaliteral{28}{\isacharparenleft}}bestsimp\ simp{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{2E}{\isachardot}}join{\isaliteral{5F}{\isacharunderscore}}def\ int{\isaliteral{2E}{\isachardot}}is{\isaliteral{5F}{\isacharunderscore}}sup{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
 \ \ \isacommand{qed}\isamarkupfalse%
diff -r de5c79682b56 -r eb8b4851b039 src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Thu Jun 23 23:12:00 2011 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Sat Jun 25 12:19:54 2011 +0200
@@ -499,7 +499,7 @@
 end
 
 interpretation x: logic_o "op &" "Not"
-  where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y"
+  where bool_logic_o: "x.lor_o(x, y) <-> x | y"
 proof -
   show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+
   show "logic_o.lor_o(op &, Not, x, y) <-> x | y"
diff -r de5c79682b56 -r eb8b4851b039 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Jun 23 23:12:00 2011 +0200
+++ b/src/Pure/Isar/expression.ML	Sat Jun 25 12:19:54 2011 +0200
@@ -797,6 +797,14 @@
 
 (*** Interpretation ***)
 
+fun read_with_extended_syntax parse_prop deps ctxt props =
+  let
+    val deps_ctxt = fold Locale.activate_declarations deps ctxt;
+  in
+    map (parse_prop deps_ctxt o snd) props |> Syntax.check_terms deps_ctxt
+      |> Variable.export_terms deps_ctxt ctxt
+  end;
+
 (** Interpretation in theories and proof contexts **)
 
 local
@@ -825,8 +833,8 @@
   let
     val ((propss, deps, export), expr_ctxt) = Proof_Context.init_global theory
       |> prep_expr expression;
+    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
 
-    val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
     val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
     val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
     val export' = Variable.export_morphism goal_ctxt expr_ctxt;
@@ -845,8 +853,8 @@
     val theory = Proof_Context.theory_of ctxt;
 
     val ((propss, deps, export), expr_ctxt) = prep_expr expression ctxt;
+    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
 
-    val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
     val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
     val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
     val export' = Variable.export_morphism goal_ctxt expr_ctxt;
@@ -904,8 +912,8 @@
     val target = intern thy raw_target;
     val target_ctxt = Named_Target.init before_exit target thy;
     val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt;
+    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
 
-    val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
     val attrss = map ((apsnd o map) (prep_attr thy) o fst) equations;
     val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
     val export' = Variable.export_morphism goal_ctxt expr_ctxt;