diff -r dc65319809cc -r 80dabcaafc38 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Tue Mar 02 14:51:40 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 02 15:10:47 2010 +0100
@@ -443,4 +443,13 @@
 1 *})
 done*)
 
+ML {*
+fun dtyp_no_of_typ _ (TFree (n, _)) = error "dtyp_no_of_typ: Illegal free"
+  | dtyp_no_of_typ _ (TVar _) = error "dtyp_no_of_typ: Illegal schematic"
+  | dtyp_no_of_typ dts (Type (tname, Ts)) =
+      case try (find_index (curry op = tname o fst)) dts of
+        NONE => error "dtyp_no_of_typ: Illegal recursion"
+      | SOME i => i
+*}
+
 end