[isabelle-dev] problem with the proof recording

[Ondřej Kunčar]

Dear All,
this refers to 3fbcfa911863.

If I use the proof recording, processing of the following theory takes 
infinite time:

theory Problem
imports Main
begin

lemma "list_all2 (Lifting.invariant P) = Lifting.invariant (list_all P)"
   apply (simp add: fun_eq_iff list_all2_def list_all_iff 
Lifting.invariant_def Ball_def)
   apply (intro allI)
   apply (induct_tac rule: list_induct2')
   apply simp_all
   apply metis
done

end

But if I change the last step from metis to fastforce, the theory goes 
through.

The problem doesn't happen if the theory is checked in jEdit, but it 
happens when processed from the command line, e.g. by using this session:

session "HOL-Problem" = "HOL-Proofs" +
   options [document = false]
   theories "$ISABELLE_HOME/src/HOL/Problem"

Does anybody have an idea why this is happening?

Thanks,
Ondrej