--- a/Nominal/nominal_dt_quot.ML	Fri Dec 31 15:37:04 2010 +0000
+++ b/Nominal/nominal_dt_quot.ML	Mon Jan 03 16:19:27 2011 +0000
@@ -671,7 +671,7 @@
 
 fun prove_strong_induct lthy induct exhausts size_thms bclausesss =
   let
-    val ((insts, [induct']), lthy') = Variable.import true [induct] lthy
+    val ((_, [induct']), lthy') = Variable.import true [induct] lthy
 
     val ([c_name, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
     val c_ty = TFree (a, @{sort fs})