src/Pure/old_goals.ML
changeset 32179 1c9c991e41c0
parent 32173 34f7b0fbe047
child 32187 cca43ca13f4f
--- a/src/Pure/old_goals.ML	Fri Jul 24 22:09:09 2009 +0200
+++ b/src/Pure/old_goals.ML	Fri Jul 24 22:17:32 2009 +0200
@@ -10,7 +10,6 @@
 
 signature OLD_GOALS =
 sig
-  val the_context: unit -> theory
   val simple_read_term: theory -> typ -> string -> term
   val read_term: theory -> string -> term
   val read_prop: theory -> string -> term
@@ -63,11 +62,6 @@
 structure OldGoals: OLD_GOALS =
 struct
 
-(* global context *)
-
-val the_context = ML_Context.the_global_context;
-
-
 (* old ways of reading terms *)
 
 fun simple_read_term thy T s =