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_function_common.ML
changeset 2974 b95a2065aa10
parent 2973 d1038e67923a
child 3120 368fc38321fc 
--- a/Nominal/nominal_function_common.ML	Mon Jul 18 17:40:13 2011 +0100
+++ b/Nominal/nominal_function_common.ML	Tue Jul 19 01:40:36 2011 +0100
@@ -58,7 +58,7 @@
         fs = map term fs, R = term R, psimps = fact psimps,
         pinducts = fact pinducts, simps = Option.map fact simps,
         inducts = Option.map fact inducts, termination = thm termination,
-        defname = name defname, is_partial=is_partial, eqvts = (*fact*) eqvts }
+        defname = name defname, is_partial=is_partial, eqvts = fact eqvts }
     end
 
 structure NominalFunctionData = Generic_Data
nominal2