Nominal/NewFv.thy
changeset 2170 1fe84fd8f8a4
parent 2163 5dc48e1af733
child 2213 231a20534950
child 2288 3b83960f9544
--- 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