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

Walther Neuper neuper at ist.tugraz.at
Wed Mar 3 11:42:16 CET 2010


re-entering a work done several years ago I now struggle with a simple 
detail for an hour -- so apologize the simplistic questions, please:

theory Test
imports Complex_Main
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);

... raises:
*** Exception- TOPLEVEL_ERROR raised
*** At command "ML".

(1) How can I get better error messages ?
(2) How do I get rid of the error message ?

Thanks a lot,
Walther Neuper                          Mailto: neuper at ist.tugraz.at
Institute for Software Technology          Tel: +43-(0)316/873-5728
University of Technology                   Fax: +43-(0)316/873-5706
Graz, Austria                             Home: www.ist.tugraz.at/neuper

More information about the isabelle-dev mailing list