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