changeset 15240 | e1e6db03beee |
parent 15013 | 34264f5e4691 |
child 15531 | 08c8dad8e399 |
--- 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");