[isabelle-dev] Pattern.match -- a minute

[Makarius]

On Wed, 3 Mar 2010, Walther Neuper wrote:

> theory Test
> imports Complex_Main
> begin
> ML {*
>  val thy = @{theory Complex_Main};
>  val parse = Syntax.read_term_global thy;
>  val (pa, tm) = (parse "a + b::real", parse "x + 2*z::real");
>  val (tye, tme) =
>       (Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv);
>  Pattern.match thy (pa, tm) (tye, tme);
> *}
> end
>
> ... raises:
> *** Exception- TOPLEVEL_ERROR raised
> *** At command "ML".
>
> Questions:
> (1) How can I get better error messages ?

By using the official Isabelle2009-1 distribution with Poly/ML 5.3.0 you 
should get something like this in the very beginning:

   *** exception MATCH raised (line 368 of "pattern.ML")
   ...

You can also say ML "Toplevel.debug := true" to get even more information.


> (2) How do I get rid of the error message ?

By making pa a pattern with schematic variables, not free ones.

Since this is a "global" example for now, you can use Logic.varify 
(although that does not work in general local situations, where parts are 
fixed and parts are arbitrary).


 	Makarius