[isabelle-dev] default cases rule

[Christian Sternagel]

Dear all,

routinely checking IsaFoR against the development version of Isabelle 
(more precisely d0dffec0da2b) I stumbled across the following 
proof-breaking inconvenience:

In Isabelle2014 and earlier we could do

notepad
begin
   fix p :: "('a × 'b × 'c)" and xs
   assume "p ∈ set xs"
   then obtain x y z where "(x, y, z) ∈ set xs"
     by (cases p) auto
end

i.e., relying on the default cases rule the proof went through.

In the development version, however, the following subgoals remain after 
"apply (cases p)"

goal (2 subgoals):
  1. ⋀z2. (⋀x y z. (x, y, z) ∈ set xs ⟹ thesis) ⟹
           xs = p # z2 ⟹ thesis
  2. ⋀z1 z2.
        (⋀x y z. (x, y, z) ∈ set xs ⟹ thesis) ⟹
        xs = z1 # z2 ⟹ p ∈ set z2 ⟹ thesis

That is, the default rule changed for assumptions of the form "_ : set _".

First question: is this intentional and what is the current default rule?

Second question: is it considered "bad form" to rely on default rules?

cheers

chris