src/Provers/Arith/cancel_numerals.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15965 f422f8283491
     1.1 --- a/src/Provers/Arith/cancel_numerals.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -59,11 +59,11 @@
     1.4  (*a left-to-right scan of terms1, seeking a term of the form #n*u, where
     1.5    #m*u is in terms2 for some m*)
     1.6  fun find_common (terms1,terms2) =
     1.7 -  let val tab2 = foldl update_by_coeff (Termtab.empty, terms2)
     1.8 +  let val tab2 = Library.foldl update_by_coeff (Termtab.empty, terms2)
     1.9        fun seek [] = raise TERM("find_common", []) 
    1.10  	| seek (t::terms) =
    1.11  	      let val (_,u) = Data.dest_coeff t 
    1.12 -	      in  if is_some (Termtab.lookup (tab2, u)) then u
    1.13 +	      in  if isSome (Termtab.lookup (tab2, u)) then u
    1.14  		  else seek terms
    1.15  	      end
    1.16    in  seek terms1 end;
    1.17 @@ -91,7 +91,7 @@
    1.18  			 Data.mk_bal (newshape(n1,terms1'), 
    1.19  				      newshape(n2,terms2')))
    1.20    in
    1.21 -      apsome Data.simplify_meta_eq
    1.22 +      Option.map Data.simplify_meta_eq
    1.23         (if n2<=n1 then 
    1.24  	    Data.prove_conv 
    1.25  	       [Data.trans_tac reshape, rtac Data.bal_add1 1,