--- a/src/Provers/simplifier.ML Wed Jun 10 17:56:57 1998 +0200
+++ b/src/Provers/simplifier.ML Wed Jun 10 18:07:07 1998 +0200
@@ -284,8 +284,8 @@
fun SIMPSET tacf state = tacf (simpset_of_sg (sign_of_thm state)) state;
fun SIMPSET' tacf i state = tacf (simpset_of_sg (sign_of_thm state)) i state;
-val simpset = simpset_of o Context.get_context;
-val simpset_ref = simpset_ref_of_sg o sign_of o Context.get_context;
+val simpset = simpset_of o Context.the_context;
+val simpset_ref = simpset_ref_of_sg o sign_of o Context.the_context;
(* change global simpset *)