# HG changeset patch
# User wenzelm
# Date 1137111183 -3600
# Node ID f37a43cec54730aff0c884d5236a845fe1adbba6
# Parent  5198a2c4c00e86192392edc313533f1903952d43
generic_setup: optional argument, defaults to Context.setup();

diff -r 5198a2c4c00e -r f37a43cec547 src/Pure/pure_thy.ML
--- 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 *)