src/HOL/MiniML/MiniML.ML

--- a/src/HOL/MiniML/MiniML.ML	Tue Feb 27 13:01:16 1996 +0100
+++ b/src/HOL/MiniML/MiniML.ML	Tue Feb 27 18:22:47 1996 +0100
@@ -22,4 +22,4 @@
 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
 (* case AppI *)
 by (Asm_full_simp_tac 1);
-bind_thm ("has_type_cl_sub", result() RS spec RS spec RS spec RS mp);
+qed_spec_mp "has_type_cl_sub";