# HG changeset patch
# User oheimb
# Date 845389979 -7200
# Node ID 076a8d2f972b8ccc44a0d15f39b435d063b0d0f5
# Parent  76ea62f720f1c82cde240ec9172f1641810b1fe0
bound o_apply theorem to thy

diff -r 76ea62f720f1 -r 076a8d2f972b src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Oct 15 10:58:59 1996 +0200
+++ b/src/HOL/simpdata.ML	Tue Oct 15 16:32:59 1996 +0200
@@ -180,7 +180,7 @@
     (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
         (fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
 
-val o_apply = prove_goalw HOL.thy [o_def] "(f o g)(x) = f(g(x))"
+val o_apply = prove_goalw HOL.thy [o_def] "(f o g) x = f (g x)"
  (fn _ => [rtac refl 1]);
 
 (*Miniscoping: pushing in existential quantifiers*)
@@ -325,7 +325,9 @@
   "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)"
+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]);