changeset 59582 | 0fbed69ff081 |
parent 59498 | 50b60f501b05 |
child 59936 | b8ffc3dc9e24 |
--- a/src/Sequents/prover.ML Tue Mar 03 19:08:04 2015 +0100 +++ b/src/Sequents/prover.ML Wed Mar 04 19:53:18 2015 +0100 @@ -157,7 +157,7 @@ (*Predicate: does the rule have n premises? *) -fun has_prems n rule = (nprems_of rule = n); +fun has_prems n rule = (Thm.nprems_of rule = n); (*Continuation-style tactical for resolution. The list of rules is partitioned into 0, 1, 2 premises.