[isabelle-dev] [isabelle] match_tac, schematic and bound variables

[Makarius]

On Sun, 18 Aug 2013, Lars Noschinski wrote:

>> Combinators like Subgoal.FOCUS have replaced a lot of old-style 
>> tinkering with goals; within the focused parts things are fixed and 
>> don't get instantiated by accident.
>
> I seem to remember a discussion on the mailing list that Subgoal.FOCUS 
> does not export schematic type variables. So this would give us another 
> not-quite correct match implementation.

I still have this on my list to look after it in further detail, but as 
far as I can tell it was about situations that are conceptially not 
allowed anyway: schematic type variables within fixed-term variables. 
The inference kernel happens to allow that in primitive rules, but almost 
everything will break down.  Type-inference is part of the syntactic 
phase, and needs to be finished before doing the actual logical 
inferencing.


 	Makarius