# HG changeset patch
# User paulson
# Date 866463933 -7200
# Node ID 8d63ff01d37e72d7fdfae28c101fe61ee8811647
# Parent  bea2faf1641d82df6fb8c0ec220b07f8fb332e27
Type constraint added to ensure that "length" refers to lists.  Maybe should
not be needed, but the translation length->size happens irrespective of types

diff -r bea2faf1641d -r 8d63ff01d37e src/HOL/MiniML/Type.ML
--- 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];