# HG changeset patch
# User wenzelm
# Date 878227310 -3600
# Node ID b9fd385981bd10778205c3046d9f20674ed8d850
# Parent  67b5552b1067fbc36771a66fc87702d6972a27b1
tuned init_data;

diff -r 67b5552b1067 -r b9fd385981bd src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Oct 30 17:00:34 1997 +0100
+++ b/src/Pure/theory.ML	Thu Oct 30 17:01:50 1997 +0100
@@ -73,7 +73,7 @@
   val add_path: string -> theory -> theory
   val add_space: string * string list -> theory -> theory
   val add_name: string -> theory -> theory
-  val init_data: string -> exn * (exn -> exn) * (exn * exn -> exn) * (exn -> unit)
+  val init_data: (string * (exn * (exn -> exn) * (exn * exn -> exn) * (exn -> unit))) list
     -> theory -> theory
   val get_data: theory -> string -> exn
   val put_data: string * exn -> theory -> theory
@@ -374,7 +374,7 @@
 
 (** additional theory data **)
 
-val init_data = curry (ext_sg Sign.init_data);
+fun init_data ds = foldl (op o) (I, map (ext_sg Sign.init_data) ds);
 val get_data = Sign.get_data o sign_of;
 val put_data = ext_sg Sign.put_data;