# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1311064846 -3600
# Node ID 967c55907ce1345959aae2887067b421cc84db2a
# Parent  a4b6e997a7c6a04da2cef771be2e1f7468aac479
merged

diff -r a4b6e997a7c6 -r 967c55907ce1 Nominal/nominal_mutual.ML
--- 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,