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);