# HG changeset patch
# User berghofe
# Date 839497504 -7200
# Node ID 0a4fbd097ce054f186342ed05572e658c8b5423c
# Parent  c7a8692290917c6092d0cba806f5aa51069905da
Removed unnecessary Addsimps.

diff -r c7a869229091 -r 0a4fbd097ce0 src/HOL/MiniML/Type.ML
--- a/src/HOL/MiniML/Type.ML	Thu Aug 08 11:34:29 1996 +0200
+++ b/src/HOL/MiniML/Type.ML	Thu Aug 08 11:45:04 1996 +0200
@@ -1,8 +1,6 @@
 open Type;
 
-Addsimps [app_subst_TVar,app_subst_Fun];
 Addsimps [mgu_eq,mgu_mg,mgu_free];
-Addsimps [free_tv_TVar,free_tv_Fun,free_tv_Nil,free_tv_Cons];
 
 (* mgu does not introduce new type variables *)
 goalw thy [new_tv_def]