src/HOL/Tools/Presburger/qelim.ML

 and proof generation for multiple quantified formulae.
 *)
 
 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
 
 end;
 
 structure Qelim : QELIM =
 struct
 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*)
 
 val qe_ex_conj = thm "qe_ex_conj";
 val qe_ex_nconj = thm "qe_ex_nconj";