# HG changeset patch
# User berghofe
# Date 1097516208 -7200
# Node ID e1e6db03beee10424a641edf1f4f8c3e26098fc2
# Parent  fb73c8154b191cf191f05c9c9c4195ab9d099ea5
Replaced the_context() by theory "Presburger" in call of invoke_oracle.

diff -r fb73c8154b19 -r e1e6db03beee src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Mon Oct 11 16:47:50 2004 +0200
+++ b/src/HOL/Integ/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");
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");