I have only used Assumption.import and co (the difference is that they work on a proper proof context), but my guess is that this comes from variables you declare locally (the one that become ?x
in the goal) that can conflict with global constants.
It's a good idea to ask such questions on the mailing list, since the best person to answer them is probably Makarius, and he boycotts Zulip.
Mathias Fleury said:
I have only used Assumption.import and co (the difference is that they work on a proper proof context), but my guess is that this comes from variables you declare locally (the one that become
?x
in the goal) that can conflict with global constants.
sorry, do you mean the import
function in Assumption
structure? I don't find that function in file src/Pure/assumption.ML
Sorry I meant Assumption.add_assumes
Last updated: Jul 15 2022 at 23:21 UTC