# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272982687 -7200
# Node ID 8bd75f2fd7b0f6856f55d4286f1d117e2684a777
# Parent  38bbccdf9ff9d9a581481519decdd2a9c70dbd8c# Parent  20be95dce64369c67a259e1fadac6d5d021bd681
merge

diff -r 20be95dce643 -r 8bd75f2fd7b0 Nominal/Tacs.thy
--- a/Nominal/Tacs.thy	Tue May 04 14:38:07 2010 +0100
+++ b/Nominal/Tacs.thy	Tue May 04 16:18:07 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