--- a/Nominal/Tacs.thy	Mon May 03 00:01:12 2010 +0100
+++ b/Nominal/Tacs.thy	Tue May 04 16:17:46 2010 +0200
@@ -158,9 +158,9 @@
 *}
 
 ML {*
-fun dtyp_no_of_typ _ (TFree (n, _)) = error "dtyp_no_of_typ: Illegal free"
+fun dtyp_no_of_typ _ (TFree (_, _)) = 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)) =
+  | dtyp_no_of_typ dts (Type (tname, _)) =
       case try (find_index (curry op = tname o fst)) dts of
         NONE => error "dtyp_no_of_typ: Illegal recursion"
       | SOME i => i