equal
deleted
inserted
replaced
157 in |
157 in |
158 map (map (map rawify_bclause)) bclauses |
158 map (map (map rawify_bclause)) bclauses |
159 end |
159 end |
160 *} |
160 *} |
161 |
161 |
162 text {* What does the prep_bn code do? Cezary's Function? *} |
162 (* strip_bn_fun takes a bn function defined by the user as a union or |
163 |
163 append of elements and returns those elements together with bn functions |
|
164 applied *) |
164 ML {* |
165 ML {* |
165 fun strip_bn_fun t = |
166 fun strip_bn_fun t = |
166 case t of |
167 case t of |
167 Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r |
168 Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r |
168 | Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r |
169 | Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r |