diff -r 040519ec99e9 -r b52e8651591f Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Mon Jan 13 15:42:10 2014 +0000 +++ b/Nominal/Nominal2.thy Thu Mar 13 09:21:31 2014 +0000 @@ -399,8 +399,8 @@ val qperm_bns = map #qconst qperm_bns_info val _ = trace_msg (K "Lifting of theorems...") - val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def - prod.cases} + val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def rel_prod_def + prod.case} val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts, qbn_inducts, qsize_eqvt, [qinduct], qexhausts, qsize_simps, qperm_bn_simps, @@ -747,6 +747,3 @@ end - - -