[isabelle-dev] inductive_set vs. 'a set

[Makarius]

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!]: "\<lbrakk>args \<in> lists (well_formed_gterm' arity);
 		length args = arity f\<rbrakk>
                \<Longrightarrow> (Apply f args) \<in> well_formed_gterm' arity"
monos lists_mono

*** Bad monotonicity theorem:
*** {x. ?A x} <= {x. ?B x} ==> {x. listsp ?A x} <= {x. listsp ?B x}
*** At command "inductive_set" (line 153 of 
"~~/doc-src/TutorialI/Inductive/Advanced.thy")


That is probably a bit too exotic to expect NEWS to say what needs to be 
done.  Nonetheless I am curious about the reason of this failure.


 	Makarius