# HG changeset patch
# User ballarin
# Date 1192789292 -7200
# Node ID ba43514068fde709bd17e527da4a6af2cfa66a84
# Parent  41ec22a00c41335da23a561e642895be8f4361ca
Interpretation equations may have name and/or attribute.

diff -r 41ec22a00c41 -r ba43514068fd doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Fri Oct 19 10:44:45 2007 +0200
+++ b/doc-src/IsarRef/generic.tex	Fri Oct 19 12:21:32 2007 +0200
@@ -394,8 +394,10 @@
   ;
   printinterps '!'? name
   ;
-  interp: thmdecl? \\ (contextexpr ('[' (inst+) ']')? |
-    name ('[' (inst+) ']')? 'where' (prop + 'and'))
+  instantiation: ('[' (inst+) ']')?
+  ;
+  interp: thmdecl? \\ (contextexpr instantiation |
+    name instantiation 'where' (thmdecl? prop + 'and'))
   ;
 \end{rail}
 
diff -r 41ec22a00c41 -r ba43514068fd src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Oct 19 10:44:45 2007 +0200
+++ b/src/Pure/Isar/class.ML	Fri Oct 19 12:21:32 2007 +0200
@@ -520,7 +520,8 @@
   in
     thy
     |> fold_map (get_remove_global_constraint o fst o snd) params
-    ||> prove_interpretation tac ((false, prfx), []) (Locale.Locale class) (inst, defs)
+    ||> prove_interpretation tac ((false, prfx), []) (Locale.Locale class)
+          (inst, map (fn def => (("", []), def)) defs)
     |-> (fn cs => fold (Sign.add_const_constraint o apsnd SOME) cs)
   end;
 
diff -r 41ec22a00c41 -r ba43514068fd src/Pure/Isar/spec_parse.ML
--- a/src/Pure/Isar/spec_parse.ML	Fri Oct 19 10:44:45 2007 +0200
+++ b/src/Pure/Isar/spec_parse.ML	Fri Oct 19 12:21:32 2007 +0200
@@ -23,7 +23,8 @@
     ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list * token list
   val locale_mixfix: token list -> mixfix * token list
   val locale_fixes: token list -> (string * string option * mixfix) list * token list
-  val locale_insts: token list -> (string option list * string list) * token list
+  val locale_insts: token list ->
+    (string option list * ((bstring * Attrib.src list) * string) list) * token list
   val class_expr: token list -> string list * token list
   val locale_expr: token list -> Locale.expr * token list
   val locale_keyword: token list -> string * token list
@@ -88,7 +89,7 @@
 
 val locale_insts =
   Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
-  -- Scan.optional (P.$$$ "where" |-- P.and_list1 P.term) [];
+  -- Scan.optional (P.$$$ "where" |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
 
 local