src/Pure/old_goals.ML
changeset 32179 1c9c991e41c0
parent 32173 34f7b0fbe047
child 32187 cca43ca13f4f
     1.1 --- a/src/Pure/old_goals.ML	Fri Jul 24 22:09:09 2009 +0200
     1.2 +++ b/src/Pure/old_goals.ML	Fri Jul 24 22:17:32 2009 +0200
     1.3 @@ -10,7 +10,6 @@
     1.4  
     1.5  signature OLD_GOALS =
     1.6  sig
     1.7 -  val the_context: unit -> theory
     1.8    val simple_read_term: theory -> typ -> string -> term
     1.9    val read_term: theory -> string -> term
    1.10    val read_prop: theory -> string -> term
    1.11 @@ -63,11 +62,6 @@
    1.12  structure OldGoals: OLD_GOALS =
    1.13  struct
    1.14  
    1.15 -(* global context *)
    1.16 -
    1.17 -val the_context = ML_Context.the_global_context;
    1.18 -
    1.19 -
    1.20  (* old ways of reading terms *)
    1.21  
    1.22  fun simple_read_term thy T s =