src/Provers/Arith/cancel_numerals.ML
changeset 15027 d23887300b96
parent 14387 e96d5c42c4b0
child 15531 08c8dad8e399
     1.1 --- a/src/Provers/Arith/cancel_numerals.ML	Thu Jul 08 19:34:18 2004 +0200
     1.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Thu Jul 08 19:34:56 2004 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4  
     1.5  functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA):
     1.6    sig
     1.7 -  val proc: Sign.sg -> thm list -> term -> thm option
     1.8 +  val proc: Sign.sg -> simpset -> term -> thm option
     1.9    end 
    1.10  =
    1.11  struct
    1.12 @@ -69,8 +69,10 @@
    1.13    in  seek terms1 end;
    1.14  
    1.15  (*the simplification procedure*)
    1.16 -fun proc sg hyps t =
    1.17 -  let (*first freeze any Vars in the term to prevent flex-flex problems*)
    1.18 +fun proc sg ss t =
    1.19 +  let
    1.20 +      val hyps = prems_of_ss ss;
    1.21 +      (*first freeze any Vars in the term to prevent flex-flex problems*)
    1.22        val (t', xs) = Term.adhoc_freeze_vars t;
    1.23        val (t1,t2) = Data.dest_bal t' 
    1.24        val terms1 = Data.dest_sum t1