# 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