Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/nominal_dt_quot.ML
changeset 3161 aa1ba91ed1ff
parent 3158 89f9d7e85e88
child 3172 4cf3a4d36799 
--- 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
nominal2