--- a/src/HOL/Tools/Presburger/qelim.ML Sat Mar 11 17:30:35 2006 +0100
+++ b/src/HOL/Tools/Presburger/qelim.ML Sat Mar 11 21:23:10 2006 +0100
@@ -8,7 +8,7 @@
signature QELIM =
sig
- val tproof_of_mlift_qelim: Sign.sg -> (term -> bool) ->
+ val tproof_of_mlift_qelim: theory -> (term -> bool) ->
(string list -> term -> thm) -> (term -> thm) ->
(term -> thm) -> term -> thm
@@ -19,7 +19,7 @@
open CooperDec;
open CooperProof;
-val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
+val cboolT = ctyp_of HOL.thy HOLogic.boolT;
(* List of the theorems to be used in the following*)