equal
deleted
inserted
replaced
277 | hmatch n = matchres tha n thb handle THM _ => hmatch (n-1) |
277 | hmatch n = matchres tha n thb handle THM _ => hmatch (n-1) |
278 in hmatch (nprems_of thb) end |
278 in hmatch (nprems_of thb) end |
279 |
279 |
280 fun hflatten t = |
280 fun hflatten t = |
281 case (concl_of t) of |
281 case (concl_of t) of |
282 Const _ $ (Const (@{const_name "op -->"}, _) $ _ $ _) => hflatten (t RS mp) |
282 Const _ $ (Const (@{const_name HOL.implies}, _) $ _ $ _) => hflatten (t RS mp) |
283 | _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t |
283 | _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t |
284 in |
284 in |
285 hflatten t |
285 hflatten t |
286 end |
286 end |
287 |
287 |