# HG changeset patch
# User ballarin
# Date 1229265784 -3600
# Node ID 76c7fc5ba849a449a2ef26ef8e5b71a29246fb32
# Parent  c3ed38de863ce022620a62da54b7129355bc88e1
Strict prefixes in locales expressions.

diff -r c3ed38de863c -r 76c7fc5ba849 src/FOL/ex/NewLocaleTest.thy
--- a/src/FOL/ex/NewLocaleTest.thy	Fri Dec 12 19:58:26 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Sun Dec 14 15:43:04 2008 +0100
@@ -421,7 +421,7 @@
 
 end
 
-interpretation x: logic_o "op &" "Not"
+interpretation x!: logic_o "op &" "Not"
   where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y"
 proof -
   show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+
@@ -431,9 +431,12 @@
 
 thm x.lor_o_def bool_logic_o
 
+lemma lor_triv: "z <-> z" ..
+
 lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast
 
-thm x.lor_triv
+thm lor_triv [where z = True] (* Check strict prefix. *)
+  x.lor_triv
 
 
 subsection {* Interpretation in proofs *}
diff -r c3ed38de863c -r 76c7fc5ba849 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Dec 12 19:58:26 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Sun Dec 14 15:43:04 2008 +0100
@@ -7,7 +7,7 @@
 signature EXPRESSION =
 sig
   datatype 'term map = Positional of 'term option list | Named of (string * 'term) list;
-  type 'term expr = (string * (string * 'term map)) list;
+  type 'term expr = (string * ((string * bool) * 'term map)) list;
   type expression = string expr * (Binding.T * string option * mixfix) list;
   type expression_i = term expr * (Binding.T * typ option * mixfix) list;
 
@@ -47,7 +47,7 @@
   Positional of 'term option list |
   Named of (string * 'term) list;
 
-type 'term expr = (string * (string * 'term map)) list;
+type 'term expr = (string * ((string * bool) * 'term map)) list;
 
 type expression = string expr * (Binding.T * string option * mixfix) list;
 type expression_i = term expr * (Binding.T * typ option * mixfix) list;
@@ -154,7 +154,7 @@
 
 (* Instantiation morphism *)
 
-fun inst_morph (parm_names, parm_types) (prfx, insts') ctxt =
+fun inst_morph (parm_names, parm_types) ((prfx, strict), insts') ctxt =
   let
     (* parameters *)
     val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
@@ -175,7 +175,7 @@
     val inst = Symtab.make insts'';
   in
     (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
-      Morphism.binding_morphism (Binding.add_prefix false prfx), ctxt')
+      Morphism.binding_morphism (Binding.add_prefix strict prfx), ctxt')
   end;
 
 
diff -r c3ed38de863c -r 76c7fc5ba849 src/Pure/Isar/spec_parse.ML
--- a/src/Pure/Isar/spec_parse.ML	Fri Dec 12 19:58:26 2008 +0100
+++ b/src/Pure/Isar/spec_parse.ML	Sun Dec 14 15:43:04 2008 +0100
@@ -104,7 +104,7 @@
 
 val rename = P.name -- Scan.option P.mixfix;
 
-val prefix = P.name --| P.$$$ ":";
+val prefix = P.name -- Scan.optional (P.$$$ "!" >> K true) false --| P.$$$ ":";
 val named = P.name -- (P.$$$ "=" |-- P.term);
 val position = P.maybe P.term;
 val instance = P.$$$ "where" |-- P.and_list1 named >> Expression.Named ||
@@ -127,7 +127,7 @@
 val locale_expression =
   let
     fun expr2 x = P.xname x;
-    fun expr1 x = (Scan.optional prefix "" -- expr2 --
+    fun expr1 x = (Scan.optional prefix ("", false) -- expr2 --
       Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
     fun expr0 x = (plus1_unless locale_keyword expr1) x;
   in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;