# HG changeset patch
# User oheimb
# Date 902931409 -7200
# Node ID b8598e4fb73eaa92c40b630ce0787bc86e40719f
# Parent  e24d15594edde2699219e8ef60730959f8c86ca2
removed superfluous o_apply

diff -r e24d15594edd -r b8598e4fb73e src/HOL/MiniML/MiniML.ML
--- a/src/HOL/MiniML/MiniML.ML	Wed Aug 12 16:15:37 1998 +0200
+++ b/src/HOL/MiniML/MiniML.ML	Wed Aug 12 16:16:49 1998 +0200
@@ -214,8 +214,6 @@
                  has_type.LETI 1);
  by (dres_inst_tac [("x","(%x. if x : free_tv A Un free_tv t then S x else TVar x) o \
 \                         (%x. if x : free_tv A then x else n + x)")] spec 1);
- val o_apply = prove_goalw HOL.thy [o_def] "(f o g) x = f (g x)"
- (fn _ => [rtac refl 1]);
  by (stac (S'_A_eq_S'_alpha_A) 1);
  by (assume_tac 1);
 by (stac S_o_alpha_typ 1);