Re: [isabelle] antiquotations

Makarius et al,

At present I have a function modify_ss (of type : MetaSimplifier.simpset -> MetaSimplifier.simpset).

It is used in a further function

fun modified_ss () = modify_ss (simpset ()) ;

Now I observe that

val simpset = simpset_of o ML_Context.the_context;

and given the previous remarks about using the_context () I assume that you wouldn't approve of using simpset (), either. Is that correct?

But if I understand the previous emails correctly, to write
fun modified_ss () = modify_ss (simpset_of @{theory}) ;
would have the effect that the simpset used was invariably one particular simpset, namely that relevant when the text "@{theory}" was interpreted.

But I want modified_ss () to take the simpset relevant at the time it is called, and modify it.

How do I define modified_ss in the approved way - using antiquotations as and where appropriate ?


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