There is another drop-out concerning 'a set (in Isabelle/05a82dd869ed):
inductive_set
well_formed_gterm' :: ('f \Rightarrow nat) \Rightarrow 'f gterm set
for arity :: 'f \Rightarrow nat
where
step[intro!]: \lbrakkargs \in lists (well_formed_gterm' arity);
length args = arity
Quoting Lawrence Paulson l...@cam.ac.uk:
I got this message several times when converting theories. There is
a workaround, but nevertheless, I think this is a bug.
Hi Larry,
the reason for this problem is the removal of the rules pred_equals_eq and
pred_subset_eq from the rule database used
