equal
deleted
inserted
replaced
135 end; |
135 end; |
136 |
136 |
137 fun make is_open rule_struct (thy, prop) cases = |
137 fun make is_open rule_struct (thy, prop) cases = |
138 let |
138 let |
139 val n = length cases; |
139 val n = length cases; |
140 val nprems = Logic.count_prems (prop, 0); |
140 val nprems = Logic.count_prems prop; |
141 fun add_case (name, concls) (cs, i) = |
141 fun add_case (name, concls) (cs, i) = |
142 ((case try (fn () => |
142 ((case try (fn () => |
143 (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of |
143 (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of |
144 NONE => (name, NONE) |
144 NONE => (name, NONE) |
145 | SOME p => (name, extract_case is_open thy p name concls)) :: cs, i - 1); |
145 | SOME p => (name, extract_case is_open thy p name concls)) :: cs, i - 1); |