# HG changeset patch
# User oheimb
# Date 845390404 -7200
# Node ID 2bfc0675c92ff842f31d4049af9813f2a2a407a7
# Parent  076a8d2f972b8ccc44a0d15f39b435d063b0d0f5
corrected `correction` of o_assoc (of version 1.14),
(this change has actually been done in the previous commit 1.25)

diff -r 076a8d2f972b -r 2bfc0675c92f src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Oct 15 16:32:59 1996 +0200
+++ b/src/HOL/simpdata.ML	Tue Oct 15 16:40:04 1996 +0200
@@ -328,7 +328,7 @@
 bind_thm ("o_apply", o_apply);
 
 qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = f o g o h"
-  (fn _=>[rtac ext 1, rtac refl 1]);
+  (fn _ => [rtac ext 1, rtac refl 1]);