equal
deleted
inserted
replaced
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) = 