Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Replaced the_context() by theory "Presburger" in call of invoke_oracle.
authorberghofe
Mon, 11 Oct 2004 19:36:48 +0200
changeset 15240 e1e6db03beee
parent 15239 fb73c8154b19
child 15241 a3949068537e
Replaced the_context() by theory "Presburger" in call of invoke_oracle.
src/HOL/Integ/presburger.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Presburger/presburger.ML file | annotate | diff | comparison | revisions 
--- 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");
--- 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");
isabelle