src/Sequents/prover.ML
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.