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

[Walther Neuper]

Hi,

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
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 ?
(2) How do I get rid of the error message ?

Thanks a lot,
Walther
-- 
------------------------------------------------------------------------
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
------------------------------------------------------------------------