799 val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _}, |
799 val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _}, |
800 {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _, |
800 {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _, |
801 loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2; |
801 loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2; |
802 |
802 |
803 val rules' = Net.merge eq_rrule (rules1, rules2); |
803 val rules' = Net.merge eq_rrule (rules1, rules2); |
804 val prems' = gen_merge_lists Thm.eq_thm_prop prems1 prems2; |
804 val prems' = merge Thm.eq_thm_prop (prems1, prems2); |
805 val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1; |
805 val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1; |
806 val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1; |
806 val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1; |
807 val congs' = merge (eq_cong o pairself #2) (congs1, congs2); |
807 val congs' = merge (eq_cong o pairself #2) (congs1, congs2); |
808 val weak' = merge (op =) (weak1, weak2); |
808 val weak' = merge (op =) (weak1, weak2); |
809 val procs' = Net.merge eq_proc (procs1, procs2); |
809 val procs' = Net.merge eq_proc (procs1, procs2); |