src/Pure/meta_simplifier.ML

           else (Thm.incr_indexes (maxt+1) thm, Thm.cterm_incr_indexes (maxt+1) elhs);
         val insts = if fo then Thm.cterm_first_order_match (elhs', eta_t')
                           else Thm.cterm_match (elhs', eta_t');
         val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
         val prop' = Thm.prop_of thm';
-        val unconditional = (Logic.count_prems (prop',0) = 0);
+        val unconditional = (Logic.count_prems prop' = 0);
         val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
       in
         if perm andalso not (termless (rhs', lhs'))
         then (trace_named_thm "Cannot apply permutative rewrite rule" ss (thm, name);
               trace_thm "Term does not become smaller:" ss thm'; NONE)