[isabelle-dev] generating fresh variables in Isabelle/ML

Christian Sternagel c-sterna at jaist.ac.jp
Sat Aug 4 04:05:13 CEST 2012

Dear all,

in changeset 206144b13849, we can (still) find the following lines in 
List.thy (which seem to indicate that this is not the right way to 
introduce a fresh variable):

   (* FIXME proper name context!? *)
   val x =
     Free (singleton (Name.variant_list
       (fold Term.add_free_names [p, e] [])) "x", dummyT);

If this is not the right way to do it, I was wondering, whether the 
following was:

   fun fresh_var ts ctxt =
       val ctxt' = fold Variable.declare_term ts ctxt
       singleton (Variable.variant_frees ctxt' []) ("x", dummyT)

   val x = Free (fresh_var [p, e] ctxt)

If not, what is the right way?



More information about the isabelle-dev mailing list