[isabelle] File.use function



Hi,

As part of my work to extend the rv tactic, I'm trying to use a file containing ML code using "File.use". The file used contained the following code :
val proof_congr = X
val proof_inst  = Y

And at the ML level, I do :

val proof_congr = []
val proof_inst = []

val _ = File.use (Path.unpack proof_hints_fn)

Even if the *isabelle* buffer in proofgeneral shows that proof_congr and proof_inst are filled with X and Y, it is actually not the case at the ML level : proof_congr and proof_inst are still the empty list :O( Why ?

Thanks for your help,
Clément






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