# HG changeset patch
# User wenzelm
# Date 940343026 -7200
# Node ID 2c65e8212115592eb2684c155d43485d5a5845d8
# Parent  01e6e05d208bb9175183514a7912dc26c51fb43c
qed_spec_mp is a mess;

diff -r 01e6e05d208b -r 2c65e8212115 src/HOL/HOL_lemmas.ML
--- a/src/HOL/HOL_lemmas.ML	Tue Oct 19 13:45:51 1999 +0200
+++ b/src/HOL/HOL_lemmas.ML	Tue Oct 19 16:23:46 1999 +0200
@@ -452,6 +452,8 @@
 
 (** strip ! and --> from proved goal while preserving !-bound var names **)
 
+(** THIS CODE IS A MESS!!! **)
+
 local
 
 (* Use XXX to avoid forall_intr failing because of duplicate variable name *)