src/Provers/Arith/combine_numerals.ML
changeset 8816 31b4fb3d8d60
parent 8799 89e9deef4bcb
child 9191 300bd596d696
equal deleted inserted replaced
8815:187547eae4c5 8816:31b4fb3d8d60
    38   sig
    38   sig
    39   val proc: Sign.sg -> thm list -> term -> thm option
    39   val proc: Sign.sg -> thm list -> term -> thm option
    40   end 
    40   end 
    41 =
    41 =
    42 struct
    42 struct
    43 
       
    44 fun listof None = []
       
    45   | listof (Some x) = [x];
       
    46 
    43 
    47 (*Remove the first occurrence of #m*u from the term list*)
    44 (*Remove the first occurrence of #m*u from the term list*)
    48 fun remove (_, _, []) = (*impossible, since #m*u was found by find_repeated*)
    45 fun remove (_, _, []) = (*impossible, since #m*u was found by find_repeated*)
    49       raise TERM("combine_numerals: remove", [])  
    46       raise TERM("combine_numerals: remove", [])  
    50   | remove (m, u, t::terms) =
    47   | remove (m, u, t::terms) =