equal
deleted
inserted
replaced
199 %in\\ |
199 %in\\ |
200 %\>fun insert\_assumptions asms = map (fn t => Asm t) asms |> insert\_ctxt;\\ |
200 %\>fun insert\_assumptions asms = map (fn t => Asm t) asms |> insert\_ctxt;\\ |
201 %\>fun insert\_environments envs = map (fn t => Env t) envs |> insert\_ctxt;\\ |
201 %\>fun insert\_environments envs = map (fn t => Env t) envs |> insert\_ctxt;\\ |
202 %end\\ |
202 %end\\ |
203 fun insert\_assumptions asms = \\ |
203 fun insert\_assumptions asms = \\ |
204 \>\>\>ContextData\alert{.map} (fn xs => distinct (data@xs));\\ |
204 \>\>\>ContextData\alert{.map} (fn xs => distinct (asms@xs));\\ |
205 \\ |
205 \\ |
206 %local\\ |
206 %local\\ |
207 %\>fun unpack\_asms (Asm t::ts) = t::(unpack\_asms ts)\\ |
207 %\>fun unpack\_asms (Asm t::ts) = t::(unpack\_asms ts)\\ |
208 %\>\>| unpack\_asms (Env \_::ts) = unpack\_asms ts\\ |
208 %\>\>| unpack\_asms (Env \_::ts) = unpack\_asms ts\\ |
209 %\>\>| unpack\_asms [] = [];\\ |
209 %\>\>| unpack\_asms [] = [];\\ |