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 3166 51c475ceaf09
parent 3161 aa1ba91ed1ff
child 3172 4cf3a4d36799 
--- 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
nominal2