Re: [isabelle] Isabelle2021-1-RC3: HELP! Bad context exception



On 14/11/2021 01:38, Peter Lammich wrote:
> 
> I'm getting an exception
> 
> exception Fail raised (line 673 of "variable.ML"): Bad context: clash
> of fresh free for bound: :001 vs. xb
> 
> I'm lost! Can someone please explain what might go wrong here, and how
> to debug and track down such errors, or point me to (ideally concise
> and understandable) documentation about what 'context discipline'
> exactly means.

Here is the announcement of the NEWS item on isabelle-dev some weeks ago:
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2021-October/017512.html

I had spent several days looking carefully at old (and some new) tools that
where violating the plain block structure that the Proof.context discipline
formalizes.

In the end it did work reasonably well: So an ancient warning could become a
proper error.


>         val thm = Goal.prove_internal ctxt [] (Thm.cterm_of ctxt
> goal_t) (fn _ => tac)

Do you see a chance to work with proper Goal.prove, instead of the internal
side-entry Goal.prove_internal?


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.