139 and flatten' (t as Const _) (names, prems) = [(t, (names, prems))] |
139 and flatten' (t as Const _) (names, prems) = [(t, (names, prems))] |
140 | flatten' (t as Free _) (names, prems) = [(t, (names, prems))] |
140 | flatten' (t as Free _) (names, prems) = [(t, (names, prems))] |
141 | flatten' (t as Abs _) (names, prems) = [(t, (names, prems))] |
141 | flatten' (t as Abs _) (names, prems) = [(t, (names, prems))] |
142 | flatten' (t as _ $ _) (names, prems) = |
142 | flatten' (t as _ $ _) (names, prems) = |
143 if is_constrt ctxt t orelse keep_functions thy t then |
143 if is_constrt ctxt t orelse keep_functions thy t then |
144 (* FIXME: constructor terms are supposed to be seen in the way the code generator |
|
145 sees constructors?*) |
|
146 [(t, (names, prems))] |
144 [(t, (names, prems))] |
147 else |
145 else |
148 case (fst (strip_comb t)) of |
146 case (fst (strip_comb t)) of |
149 Const (@{const_name "If"}, _) => |
147 Const (@{const_name "If"}, _) => |
150 (let |
148 (let |