# HG changeset patch
# User wenzelm
# Date 1248466652 -7200
# Node ID 1c9c991e41c01a72e484ddad815d9e814790ace9
# Parent  0261c3eaae4110143491d0cc19b0c3600b5ac570
eliminated the_context;

diff -r 0261c3eaae41 -r 1c9c991e41c0 src/Pure/old_goals.ML
--- 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 =