# HG changeset patch
# User paulson
# Date 843726859 -7200
# Node ID 738bb98d65ec78a84b4d97f9b6445ae9c4873984
# Parent  0f11f625063b9a164552c392c9074a6f647cf7be
Last working version prior to addition of "lost" component

diff -r 0f11f625063b -r 738bb98d65ec src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Wed Sep 25 18:01:18 1996 +0200
+++ b/src/HOL/Auth/Message.ML	Thu Sep 26 10:34:19 1996 +0200
@@ -202,6 +202,8 @@
                       addIs  [parts_insertI]) 1);
 qed "parts_cut_eq";
 
+Addsimps [parts_cut_eq];
+
 
 (** Rewrite rules for pulling out atomic messages **)