diff -r fb73c8154b19 -r e1e6db03beee src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Mon Oct 11 16:47:50 2004 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML	Mon Oct 11 19:36:48 2004 +0200
@@ -31,7 +31,7 @@
 (* Invoking the oracle *)
 
 fun pres_oracle sg t = 
-  invoke_oracle (the_context()) "presburger_oracle" 
+  invoke_oracle (theory "Presburger") "presburger_oracle" 
      (sg, CooperDec.COOPER_ORACLE t) ;
 
 val presburger_ss = simpset_of (theory "Presburger");