*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Variable 'b::{} not of sort type*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Wed, 31 Oct 2012 09:10:10 +0100*In-reply-to*: <94474096-5615-4E2F-AB19-5BB43F4C8EC9@nicta.com.au>*References*: <94474096-5615-4E2F-AB19-5BB43F4C8EC9@nicta.com.au>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.7) Gecko/20120922 Icedove/10.0.7

On 31.10.2012 07:14, Gerwin Klein wrote:

We recently came across this surprising (to me) behaviour in Isabelle 2012 (also development version): lemma "f x = f x" apply (insert refl[where t="x"]) *** Type unification failed: Variable 'b::{} not of sort type *** *** Failed to meet type constraint: *** *** Term: x :: 'b *** Type: ??'a

whereas the workaround lemma "f x = f (x::'b)" apply (insert refl[where t="x"]) works as expected.

Fixing the type of f should also help.

**Follow-Ups**:**Re: [isabelle] Variable 'b::{} not of sort type***From:*Gerwin Klein

**References**:**[isabelle] Variable 'b::{} not of sort type***From:*Gerwin Klein

- Previous by Date: Re: [isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized
- Next by Date: Re: [isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized
- Previous by Thread: [isabelle] Variable 'b::{} not of sort type
- Next by Thread: Re: [isabelle] Variable 'b::{} not of sort type
- Cl-isabelle-users October 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list