Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned init_data;
authorwenzelm
Thu, 30 Oct 1997 17:01:50 +0100
changeset 4048 b9fd385981bd
parent 4047 67b5552b1067
child 4049 b2a70d318df2
tuned init_data;
src/Pure/theory.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle