diff -r 64ed05609568 -r 8b3b6d09ef40 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Sep 25 17:06:14 2007 +0200
+++ b/src/Pure/pure_thy.ML	Tue Sep 25 17:06:18 2007 +0200
@@ -147,7 +147,7 @@
 (** dataype theorems **)
 
 structure TheoremsData = TheoryDataFun
-(struct
+(
   type T =
    {theorems: thm list NameSpace.table,
     index: FactIndex.T} ref;
@@ -159,7 +159,7 @@
   fun copy (ref x) = ref x;
   val extend = mk_empty;
   fun merge _ = mk_empty;
-end);
+);
 
 val get_theorems_ref = TheoremsData.get;
 val get_theorems = ! o get_theorems_ref;