[isabelle] schematic variables and antiquotations



Hello,

I'm trying to do some experiments with Isabelle 2009 - I'm writing a function to "zip-to" a particular subterm. I would like specify the subterm in a way that can involve schematic variables, much like the find feature which lets schematic variables be used to find theorems matching a pattern.

So here's what I'm doing...

(** START **)
theory norm
imports Main
uses "tools.ML"
begin

local_setup {* ProofContext.set_mode ProofContext.mode_schematic *}

ML {*
val x = zip_to_matching_subterm @{context} [] @{term "?x + ?y"} 0 @{term "1 + 2 + 3 + 4"};
*}
(** END **)

but here I get:

*** Unbound schematic variable: ?x
*** At command "ML".

Can I get the antiquotation to read schematic terms? Should I create a new kind of antiquotation? (is that easy?) Suggestions very welcome,

cheers,
lucas

--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.