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

[Christian Sternagel]

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 =
     let
       val ctxt' = fold Variable.declare_term ts ctxt
     in
       singleton (Variable.variant_frees ctxt' []) ("x", dummyT)
     end

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

If not, what is the right way?

cheers

chris