diff -r 31c64dd4c95a -r 51c475ceaf09 Nominal/nominal_dt_quot.ML
--- a/Nominal/nominal_dt_quot.ML	Mon Apr 30 15:45:23 2012 +0100
+++ b/Nominal/nominal_dt_quot.ML	Tue May 01 12:16:04 2012 +0100
@@ -105,7 +105,7 @@
       |> Local_Theory.exit_global
       |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) 
   
-    val (qs, lthy2) = define_qconsts qtys perm_specs lthy1
+    val (_, lthy2) = define_qconsts qtys perm_specs lthy1
 
     val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2