diff -r 687369ae8f81 -r 1fe84fd8f8a4 Nominal/NewFv.thy --- a/Nominal/NewFv.thy Fri May 21 10:47:07 2010 +0200 +++ b/Nominal/NewFv.thy Fri May 21 10:47:45 2010 +0200 @@ -290,4 +290,21 @@ end *} +(**************************************************) + +datatype foo = + C1 nat +| C2 foo int + +(* +ML {* +fun mk_body descr sorts fv_ty_map dtyp = +let + val nth_dtyp_constr_tys descr sorts +in + true end +*} +*) + +end