ProgTutorial/FirstSteps.thy
changeset 419 2e199c5faf76
parent 417 5f00958e3c7b
child 420 0bcd598d2587
--- a/ProgTutorial/FirstSteps.thy	Sun Mar 07 21:15:05 2010 +0100
+++ b/ProgTutorial/FirstSteps.thy	Wed Apr 07 11:12:12 2010 +0200
@@ -569,8 +569,8 @@
 *}
 
 setup %gray {* let
-  val (ival1, setup_ival1) = Attrib.config_int "ival1" 1
-  val (ival2, setup_ival2) = Attrib.config_int "ival2" 2
+  val (ival1, setup_ival1) = Attrib.config_int "ival1" (K 1)
+  val (ival2, setup_ival2) = Attrib.config_int "ival2" (K 2)
 in
   setup_ival1 #>
   setup_ival2
@@ -1331,9 +1331,9 @@
   values can be declared by
 *}
 
-ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false
-val (ival, setup_ival) = Attrib.config_int "ival" 0
-val (sval, setup_sval) = Attrib.config_string "sval" "some string" *}
+ML{*val (bval, setup_bval) = Attrib.config_bool "bval" (K false)
+val (ival, setup_ival) = Attrib.config_int "ival" (K 0)
+val (sval, setup_sval) = Attrib.config_string "sval" (K "some string") *}
 
 text {* 
   where each value needs to be given a default. To enable these values on the