Replaced the_context() by theory "Presburger" in call of invoke_oracle.
authorberghofe
Mon Oct 11 19:36:48 2004 +0200 (2004-10-11)
changeset 15240e1e6db03beee
parent 15239 fb73c8154b19
child 15241 a3949068537e
Replaced the_context() by theory "Presburger" in call of invoke_oracle.
src/HOL/Integ/presburger.ML
src/HOL/Tools/Presburger/presburger.ML
     1.1 --- a/src/HOL/Integ/presburger.ML	Mon Oct 11 16:47:50 2004 +0200
     1.2 +++ b/src/HOL/Integ/presburger.ML	Mon Oct 11 19:36:48 2004 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  (* Invoking the oracle *)
     1.5  
     1.6  fun pres_oracle sg t = 
     1.7 -  invoke_oracle (the_context()) "presburger_oracle" 
     1.8 +  invoke_oracle (theory "Presburger") "presburger_oracle" 
     1.9       (sg, CooperDec.COOPER_ORACLE t) ;
    1.10  
    1.11  val presburger_ss = simpset_of (theory "Presburger");
     2.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Mon Oct 11 16:47:50 2004 +0200
     2.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Mon Oct 11 19:36:48 2004 +0200
     2.3 @@ -31,7 +31,7 @@
     2.4  (* Invoking the oracle *)
     2.5  
     2.6  fun pres_oracle sg t = 
     2.7 -  invoke_oracle (the_context()) "presburger_oracle" 
     2.8 +  invoke_oracle (theory "Presburger") "presburger_oracle" 
     2.9       (sg, CooperDec.COOPER_ORACLE t) ;
    2.10  
    2.11  val presburger_ss = simpset_of (theory "Presburger");