equal
deleted
inserted
replaced
18 |
18 |
19 fun name_hyps (arg as ((cases, consumes), th)) = |
19 fun name_hyps (arg as ((cases, consumes), th)) = |
20 if not(forall (null o #2 o #1) cases) then arg |
20 if not(forall (null o #2 o #1) cases) then arg |
21 else |
21 else |
22 let |
22 let |
23 val (prems, concl) = Logic.strip_horn (prop_of th); |
23 val (prems, concl) = Logic.strip_horn (Thm.prop_of th); |
24 val prems' = drop consumes prems; |
24 val prems' = drop consumes prems; |
25 val ps = preds_of concl; |
25 val ps = preds_of concl; |
26 |
26 |
27 fun hname_of t = |
27 fun hname_of t = |
28 if exists_subterm (member (op =) ps) t |
28 if exists_subterm (member (op =) ps) t |