# HG changeset patch
# User wenzelm
# Date 1190732778 -7200
# Node ID 8b3b6d09ef40a0fa825652e84671e20e9c8727e8
# Parent  64ed056095683e815a80dc642d3ed46d8d33a3e4
tuned functor application;

diff -r 64ed05609568 -r 8b3b6d09ef40 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Sep 25 17:06:14 2007 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue Sep 25 17:06:18 2007 +0200
@@ -201,13 +201,13 @@
 (* naming *)
 
 structure Configs = TheoryDataFun
-(struct
+(
   type T = Config.value Config.T Symtab.table;
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
   fun merge _ = Symtab.merge (K true);
-end);
+);
 
 fun print_configs ctxt =
   let
diff -r 64ed05609568 -r 8b3b6d09ef40 src/Pure/Isar/instance.ML
--- a/src/Pure/Isar/instance.ML	Tue Sep 25 17:06:14 2007 +0200
+++ b/src/Pure/Isar/instance.ML	Tue Sep 25 17:06:18 2007 +0200
@@ -17,11 +17,11 @@
 structure Instance : INSTANCE =
 struct
 
-structure Instantiation = ProofDataFun(
-struct
+structure Instantiation = ProofDataFun
+(
   type T = ((string * (string * sort) list) * sort) list * ((string * typ) * string) list;
   fun init _ = ([], []);
-end);
+);
 
 local
 
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;
diff -r 64ed05609568 -r 8b3b6d09ef40 src/Tools/code/code_funcgr.ML
--- a/src/Tools/code/code_funcgr.ML	Tue Sep 25 17:06:14 2007 +0200
+++ b/src/Tools/code/code_funcgr.ML	Tue Sep 25 17:06:18 2007 +0200
@@ -328,7 +328,7 @@
 end; (*local*)
 
 structure Funcgr = CodeDataFun
-(struct
+(
   type T = T;
   val empty = Graph.empty;
   fun merge _ _ = Graph.empty;
@@ -336,7 +336,7 @@
     | purge _ (SOME cs) funcgr =
         Graph.del_nodes ((Graph.all_preds funcgr 
           o filter (can (Graph.get_node funcgr))) cs) funcgr;
-end);
+);
 
 fun make thy =
   Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);
diff -r 64ed05609568 -r 8b3b6d09ef40 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Tue Sep 25 17:06:14 2007 +0200
+++ b/src/Tools/nbe.ML	Tue Sep 25 17:06:18 2007 +0200
@@ -82,12 +82,12 @@
 (* global functions store *)
 
 structure Nbe_Functions = CodeDataFun
-(struct
+(
   type T = Univ Symtab.table;
   val empty = Symtab.empty;
   fun merge _ = Symtab.merge (K true);
   fun purge _ _ _ = Symtab.empty;
-end);
+);
 
 (* sandbox communication *)