--- a/src/Pure/Isar/locale.ML Mon Jan 24 16:25:36 2005 +0100
+++ b/src/Pure/Isar/locale.ML Mon Jan 24 17:56:18 2005 +0100
@@ -71,7 +71,7 @@
((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
theory -> theory * (bstring * thm list) list
val note_thmss: string -> xstring ->
- ((bstring * context attribute list) * (xstring * context attribute list) list) list ->
+ ((bstring * context attribute list) * (thmref * context attribute list) list) list ->
theory -> theory * (bstring * thm list) list
val note_thmss_i: string -> string ->
((bstring * context attribute list) * (thm list * context attribute list) list) list ->
@@ -106,7 +106,7 @@
datatype 'a elem_expr =
Elem of 'a | Expr of expr;
-type 'att element = (string, string, string, 'att) elem;
+type 'att element = (string, string, thmref, 'att) elem;
type 'att element_i = (typ, term, thm list, 'att) elem;
type locale =