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_mutual.ML
changeset 2978 967c55907ce1
parent 2975 c62e26830420
child 2981 c8acaded1777 
--- a/Nominal/nominal_mutual.ML	Tue Jul 19 08:34:54 2011 +0100
+++ b/Nominal/nominal_mutual.ML	Tue Jul 19 09:40:46 2011 +0100
@@ -300,7 +300,7 @@
     val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
     val mtermination = full_simplify rew_ss termination
     val mdomintros = Option.map (map (full_simplify rew_ss)) domintros
-    val meqvts = mk_meqvts lthy eqvt all_f_defs
+    val meqvts = [eqvt] (*mk_meqvts lthy eqvt all_f_defs*)
  in
     NominalFunctionResult { fs=fs, G=G, R=R,
       psimps=mpsimps, simple_pinducts=minducts,
nominal2