# HG changeset patch
# User haftmann
# Date 1265634770 -3600
# Node ID 6eb917794a5cf4ce38835616df6033b10c622435
# Parent  e682bb58707146c3ae956db651488d966eeb3328
avoid upto in generated code (is infix operator in library.ML)

diff -r e682bb587071 -r 6eb917794a5c src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- 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
diff -r e682bb587071 -r 6eb917794a5c src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- 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} () *}