diff -r 029f8aabed12 -r 5dc48e1af733 Nominal/NewFv.thy --- a/Nominal/NewFv.thy Tue May 18 14:40:05 2010 +0100 +++ b/Nominal/NewFv.thy Wed May 19 12:43:38 2010 +0100 @@ -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