# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1412695043 -3600
# Node ID 789ade899a53a3c8616dab23697e9d09f5e929ee
# Parent  768851ac930b0fa89e7451a74c20f1db4d82a425
added type information to produce the expected result with value

diff -r 768851ac930b -r 789ade899a53 thys/CountSnoc.thy
--- a/thys/CountSnoc.thy	Tue Oct 07 12:48:56 2014 +0100
+++ b/thys/CountSnoc.thy	Tue Oct 07 16:17:23 2014 +0100
@@ -19,9 +19,9 @@
   if x = y then Suc(count_list x xs) 
   else count_list x xs)"
 
-value "count_list 1 [1,1,1]"
-value "count_list 1 [2,2,2]"
-value "count_list 2 [2,2,1]"
+value "count_list (1::nat) [1,1,1]"
+value "count_list (1::nat) [2,2,2]"
+value "count_list (2::nat) [2,2,1]"