Dear Walther, About your second question: there is a section about using the function Pattern.match in the Programming Tutorial ([1], Section 3.3). It should explain how to do such pattern match examples. The main contortion below probably comes from the parsing of input. Since the antiquotation @{term ...} does not allow schematic variables, I written a small antiquotation @{term_pat ...} that is explained section 2.4 and which allows such input terms to be given directly. All should be conveniently referenced.
Hope this helps, Christian [1] http://isabelle.in.tum.de/nominal/activities/idp/ Walther Neuper writes: > 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 > ------------------------------------------------------------------------ > _______________________________________________ > Isabelle-dev mailing list > Isabelle-dev at mailbroy.informatik.tu-muenchen.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev