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.
generic_setup: optional argument, defaults to Context.setup();
authorwenzelm
Fri, 13 Jan 2006 01:13:03 +0100
changeset 18666 f37a43cec547
parent 18665 5198a2c4c00e
child 18667 85d04c28224a
generic_setup: optional argument, defaults to Context.setup();
src/Pure/pure_thy.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/pure_thy.ML	Fri Jan 13 01:13:02 2006 +0100
+++ b/src/Pure/pure_thy.ML	Fri Jan 13 01:13:03 2006 +0100
@@ -77,7 +77,7 @@
     theory -> thm list list * theory
   val add_defss_i: bool -> ((bstring * term list) * theory attribute list) list ->
     theory -> thm list list * theory
-  val generic_setup: string -> theory -> theory
+  val generic_setup: string option -> theory -> theory
   val add_oracle: bstring * string * string -> theory -> theory
 end;
 
@@ -461,8 +461,9 @@
 
 (* generic_setup *)
 
-val generic_setup =
-  Context.use_let "val setup: (theory -> theory) list" "Library.apply setup";
+fun generic_setup NONE = (fn thy => thy |> Library.apply (Context.setup ()))
+  | generic_setup (SOME txt) =
+      Context.use_let "val setup: (theory -> theory) list" "Library.apply setup" txt;
 
 
 (* add_oracle *)
isabelle