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 3046 9b0324e1293b
parent 3045 d0ad264f8c4f
child 3056 756f48abb40a 
--- a/Nominal/nominal_dt_quot.ML	Thu Nov 03 13:19:23 2011 +0000
+++ b/Nominal/nominal_dt_quot.ML	Mon Nov 07 13:58:18 2011 +0000
@@ -85,7 +85,7 @@
   
     val (qs, lthy2) = define_qconsts qtys perm_specs lthy1
 
-    val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws (Local_Theory.target_of lthy2)
+    val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2
 
     val lifted_perm_laws = 
       map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws'
nominal2