# HG changeset patch
# User pusch
# Date 837616554 -7200
# Node ID 35f22792aade50c7e83613f26f8d8f72ff75f2ba
# Parent  b07ee188f06124e37bcf2b1369034073172362c7
Corrected o_assoc lemma

diff -r b07ee188f061 -r 35f22792aade src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Jul 17 17:12:33 1996 +0200
+++ b/src/HOL/simpdata.ML	Wed Jul 17 17:15:54 1996 +0200
@@ -203,5 +203,5 @@
   "f(if c then x else y) = (if c then f x else f y)" 
   (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
 
-qed_goalw "o_assoc" HOL.thy [o_def] "(f o g) o h = (f o g o h)"
+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]);