equal
deleted
inserted
replaced
68 type clasimpset = claset * simpset; |
68 type clasimpset = claset * simpset; |
69 |
69 |
70 fun get_css context = (Classical.get_cs context, Simplifier.get_ss context); |
70 fun get_css context = (Classical.get_cs context, Simplifier.get_ss context); |
71 |
71 |
72 fun map_css f context = |
72 fun map_css f context = |
73 let val (cs', ss') = f (get_css context) |
73 let |
74 in context |> Classical.map_cs (K cs') |> Simplifier.map_ss (K ss') end; |
74 val (cs, ss) = get_css context; |
|
75 val (cs', ss') = f (cs, Simplifier.context (Context.proof_of context) ss); |
|
76 in |
|
77 context |
|
78 |> Classical.map_cs (K cs') |
|
79 |> Simplifier.map_ss (K (Simplifier.inherit_context ss ss')) |
|
80 end; |
75 |
81 |
76 fun clasimpset_of ctxt = (Classical.claset_of ctxt, Simplifier.simpset_of ctxt); |
82 fun clasimpset_of ctxt = (Classical.claset_of ctxt, Simplifier.simpset_of ctxt); |
77 |
83 |
78 |
84 |
79 (* clasimpset operations *) |
85 (* clasimpset operations *) |