[isabelle-dev] [isabelle] Higher-order matching against schematic variables

[Makarius]

On Fri, 19 Nov 2010, Lawrence Paulson wrote:

> Indeed I find the code peculiar, in that it delivers the higher-order 
> matchers followed by the first-order ones. But these are different 
> things. And I imagine there is often redundancy.

Unify.matchers started as Isar-specific ProofContext.simult_matches many 
years ago.  The main idea is to make Isar "is" patterns behave as sensible 
as possible.  Browsing a little through the changset history, you can see 
how I have struggled with it over the years.

In 2000 everything is still relatively plain and simple, e.g. see 
http://isabelle.in.tum.de/repos/isabelle/annotate/4da940d100f5/src/Pure/Isar/proof_context.ML#l564

Around 2006 I've made some further revisions, and things became much more 
complicated:

   227a01b8db80 moved to unify.ML

   8257e52164a1 matchers: try pattern_matchers only *after* general
     matching (The pattern version is not a faithful approximation because
     it falls back on first-order matching!);

   9e7d3d06c643 matchers: fall back on plain first_order_matchers, not pattern;

Etc.  Maybe you find some more explanations.


 	Makarius