# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272982666 -7200
# Node ID 38bbccdf9ff9d9a581481519decdd2a9c70dbd8c
# Parent  17684f7eaeb99e8826ca0457e511b3f397082bc3
Minor

diff -r 17684f7eaeb9 -r 38bbccdf9ff9 Nominal/Tacs.thy
--- 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