diff -r 8bda1d947df3 -r aa1ba91ed1ff Nominal/nominal_dt_quot.ML
--- a/Nominal/nominal_dt_quot.ML	Thu Apr 12 01:39:54 2012 +0100
+++ b/Nominal/nominal_dt_quot.ML	Fri Apr 20 15:28:35 2012 +0200
@@ -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