Stream: General

Topic: Bad theory import FuncSet

view this post on Zulip Jun Xu (Mar 15 2026 at 09:02):

I have a theory import in a file "PATH_TO_PROJECT/xxx.thy" named "HOL-Library.Funcset". This file is supposed to lie in %ISABELLE_HOME%\src\HOL\Library\ . But when I open up the file in Isabelle it says:

Bad theory name "FuncSet" for file "Funcset.thy"

I looked around and there is no file "Funcset.thy" anywhere. And this error only happens after I call "isabelle components -u ..." to use the AFP entries. I suspect a name conflict but could not find the exact conflict.

Has anyone experienced this before?

view this post on Zulip Mathias Fleury (Mar 15 2026 at 09:05):

Capitalization matters in the names

view this post on Zulip Mathias Fleury (Mar 15 2026 at 09:06):

You should import HOL-Library.FuncSet

view this post on Zulip Jun Xu (Mar 15 2026 at 09:08):

Thank you Mathias. I don't know why I overlooked this.

Last updated: Mar 20 2026 at 05:16 UTC