--- 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;