# HG changeset patch
# User paulson
# Date 898866640 -7200
# Node ID e4aa78d1312fdf346f39150c2a4604841b2e273b
# Parent  ee8a754f198187fba03b1bf4a965826c1b247b11
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc

diff -r ee8a754f1981 -r e4aa78d1312f src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Thu Jun 25 16:28:41 1998 +0200
+++ b/src/HOL/Prod.ML	Fri Jun 26 15:10:40 1998 +0200
@@ -404,7 +404,8 @@
 AddSEs [fst_imageE, snd_imageE, prod_fun_imageE];
 
 
-(*simplification procedure for unit_eq; cannot use this rule directly -- loops!*)
+(*simplification procedure for unit_eq.
+  Cannot use this rule directly -- it loops!*)
 local
   val unit_pat = Thm.cterm_of (sign_of thy) (Free ("x", HOLogic.unitT));
   val unit_meta_eq = standard (mk_meta_eq unit_eq);
@@ -418,6 +419,15 @@
 Addsimprocs [unit_eq_proc];
 
 
+(*This rewrite counters the effect of unit_eq_proc on (%u::unit. f u),
+  replacing it by f rather than by %u.f(). *)
+Goal "(%u::unit. f()) = f";
+by (rtac ext 1);
+by (Simp_tac 1);
+qed "unit_abs_eta_conv";
+Addsimps [unit_abs_eta_conv];
+
+
 structure Prod_Syntax =		(* FIXME eliminate (use HOLogic instead!) *)
 struct