Type constraint added to ensure that "length" refers to lists. Maybe should
not be needed, but the translation length->size happens irrespective of types

--- a/src/HOL/MiniML/Type.ML	Mon Jun 16 14:24:11 1997 +0200
+++ b/src/HOL/MiniML/Type.ML	Mon Jun 16 14:25:33 1997 +0200
@@ -651,7 +651,8 @@
 
 (* lemmata for substitutions *)
 
-goalw Type.thy [app_subst_list] "length ($ S A) = length A";
+goalw Type.thy [app_subst_list] 
+   "!!A:: ('a::type_struct) list. length ($ S A) = length A";
 by (Simp_tac 1);
 qed "length_app_subst_list";
 Addsimps [length_app_subst_list];