431 fun add_asms(ss,thm,a,anet,ats,cs) = |
431 fun add_asms(ss,thm,a,anet,ats,cs) = |
432 let val As = strip_varify(nth_subgoal i thm, a, []); |
432 let val As = strip_varify(nth_subgoal i thm, a, []); |
433 val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As; |
433 val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As; |
434 val new_rws = List.concat(map mk_rew_rules thms); |
434 val new_rws = List.concat(map mk_rew_rules thms); |
435 val rwrls = map mk_trans (List.concat(map mk_rew_rules thms)); |
435 val rwrls = map mk_trans (List.concat(map mk_rew_rules thms)); |
436 val anet' = foldr lhs_insert_thm anet rwrls |
436 val anet' = List.foldr lhs_insert_thm anet rwrls |
437 in if !tracing andalso not(null new_rws) |
437 in if !tracing andalso not(null new_rws) |
438 then (writeln"Adding rewrites:"; Display.prths new_rws; ()) |
438 then (writeln"Adding rewrites:"; Display.prths new_rws; ()) |
439 else (); |
439 else (); |
440 (ss,thm,anet',anet::ats,cs) |
440 (ss,thm,anet',anet::ats,cs) |
441 end; |
441 end; |