src/Pure/context.ML
changeset 26435 bdce320cd426
parent 26428 5b2beca2087d
child 26463 9283b4185fdf
     1.1 --- a/src/Pure/context.ML	Thu Mar 27 15:32:12 2008 +0100
     1.2 +++ b/src/Pure/context.ML	Thu Mar 27 15:32:15 2008 +0100
     1.3 @@ -68,9 +68,6 @@
     1.4    val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
     1.5    val >> : (theory -> theory) -> unit
     1.6    val >>> : (theory -> 'a * theory) -> 'a
     1.7 -  (*delayed setup*)
     1.8 -  val add_setup: (theory -> theory) -> unit
     1.9 -  val setup: unit -> theory -> theory
    1.10  end;
    1.11  
    1.12  signature PRIVATE_CONTEXT =
    1.13 @@ -537,17 +534,6 @@
    1.14  
    1.15  val _ = set_thread_data (SOME (Theory pre_pure_thy));
    1.16  
    1.17 -
    1.18 -
    1.19 -(** delayed theory setup **)
    1.20 -
    1.21 -local
    1.22 -  val setup_fn = ref (I: theory -> theory);
    1.23 -in
    1.24 -  fun add_setup f = CRITICAL (fn () => setup_fn := (! setup_fn #> f));
    1.25 -  fun setup () = CRITICAL (fn () => let val f = ! setup_fn in setup_fn := I; f end);
    1.26 -end;
    1.27 -
    1.28  end;
    1.29  
    1.30  structure BasicContext: BASIC_CONTEXT = Context;