equal
deleted
inserted
replaced
189 in |
189 in |
190 map (map (map rawify_bclause)) bclauses |
190 map (map (map rawify_bclause)) bclauses |
191 end |
191 end |
192 *} |
192 *} |
193 |
193 |
194 text {* What does the prep_bn code do ? *} |
194 text {* What does the prep_bn code do? Cezary's Function? *} |
195 |
195 |
196 ML {* |
196 ML {* |
197 fun strip_bn_fun t = |
197 fun strip_bn_fun t = |
198 case t of |
198 case t of |
199 Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r |
199 Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r |