--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Mon Feb 08 14:08:32 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Mon Feb 08 14:12:50 2010 +0100
@@ -629,6 +629,8 @@
return a
done"
+code_reserved SML upto
+
ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
export_code qsort in SML_imp module_name QSort
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Feb 08 14:08:32 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Feb 08 14:12:50 2010 +0100
@@ -986,6 +986,8 @@
return zs
done)"
+code_reserved SML upto
+
ML {* @{code test_1} () *}
ML {* @{code test_2} () *}
ML {* @{code test_3} () *}