src/Pure/context.ML
changeset 26435 bdce320cd426
parent 26428 5b2beca2087d
child 26463 9283b4185fdf
--- a/src/Pure/context.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/context.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -68,9 +68,6 @@
   val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
   val >> : (theory -> theory) -> unit
   val >>> : (theory -> 'a * theory) -> 'a
-  (*delayed setup*)
-  val add_setup: (theory -> theory) -> unit
-  val setup: unit -> theory -> theory
 end;
 
 signature PRIVATE_CONTEXT =
@@ -537,17 +534,6 @@
 
 val _ = set_thread_data (SOME (Theory pre_pure_thy));
 
-
-
-(** delayed theory setup **)
-
-local
-  val setup_fn = ref (I: theory -> theory);
-in
-  fun add_setup f = CRITICAL (fn () => setup_fn := (! setup_fn #> f));
-  fun setup () = CRITICAL (fn () => let val f = ! setup_fn in setup_fn := I; f end);
-end;
-
 end;
 
 structure BasicContext: BASIC_CONTEXT = Context;