src/Provers/Arith/combine_numerals.ML
changeset 17224 a78339014063
parent 16973 b2a894562b8f
child 17412 e26cb20ef0cc
equal deleted inserted replaced
17223:430edc6b7826 17224:a78339014063
    55   #m*u is already in terms for some m*)
    55   #m*u is already in terms for some m*)
    56 fun find_repeated (tab, _, []) = raise TERM("find_repeated", []) 
    56 fun find_repeated (tab, _, []) = raise TERM("find_repeated", []) 
    57   | find_repeated (tab, past, t::terms) =
    57   | find_repeated (tab, past, t::terms) =
    58       case try Data.dest_coeff t of
    58       case try Data.dest_coeff t of
    59 	  SOME(n,u) => 
    59 	  SOME(n,u) => 
    60 	      (case Termtab.lookup (tab, u) of
    60 	      (case Termtab.curried_lookup tab u of
    61 		  SOME m => (u, m, n, rev (remove (m,u,past)) @ terms)
    61 		  SOME m => (u, m, n, rev (remove (m,u,past)) @ terms)
    62 		| NONE => find_repeated (Termtab.update ((u,n), tab), 
    62 		| NONE => find_repeated (Termtab.curried_update (u, n) tab, 
    63 					 t::past,  terms))
    63 					 t::past,  terms))
    64 	| NONE => find_repeated (tab, t::past, terms);
    64 	| NONE => find_repeated (tab, t::past, terms);
    65 
    65 
    66 (*the simplification procedure*)
    66 (*the simplification procedure*)
    67 fun proc thy ss t =
    67 fun proc thy ss t =