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

Makarius makarius at sketis.net
Fri Nov 19 22:35:39 CET 2010

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 

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

   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.


More information about the isabelle-dev mailing list