| changeset 1901 | 0a4fbd097ce0 |
| parent 1751 | 946efd210837 |
| child 2031 | 03a843f0f447 |
--- 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]