# HG changeset patch
# User wenzelm
# Date 898781657 -7200
# Node ID beb21c000cb1c2dbf01f5967633094db9c9ad654
# Parent  e03460289797bbc8624618b2bc23910274a1f2c4
added unit_eq simplification procedure;

diff -r e03460289797 -r beb21c000cb1 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Thu Jun 25 15:33:30 1998 +0200
+++ b/src/HOL/Prod.ML	Thu Jun 25 15:34:17 1998 +0200
@@ -391,6 +391,7 @@
 by (assume_tac 1);
 qed "snd_imageE";
 
+
 (** Exhaustion rule for unit -- a degenerate form of induction **)
 
 Goalw [Unity_def]
@@ -402,7 +403,22 @@
 AddIs  [fst_imageI, snd_imageI, prod_fun_imageI];
 AddSEs [fst_imageE, snd_imageE, prod_fun_imageE];
 
-structure Prod_Syntax =
+
+(*simplification procedure for unit_eq; cannot use this rule directly -- 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);
+  fun proc _ _ t =
+    if HOLogic.is_unit t then None
+    else Some unit_meta_eq;
+in
+  val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc;
+end;
+
+Addsimprocs [unit_eq_proc];
+
+
+structure Prod_Syntax =		(* FIXME eliminate (use HOLogic instead!) *)
 struct
 
 val unitT = Type("unit",[]);