# HG changeset patch
# User haftmann
# Date 1356686759 -3600
# Node ID 1ea90e8046dc293fa6c8c640cf0d99d304b4b829
# Parent  264ece81df93877036668dc153c6961b99303d14
code checking for Scala is mandatory, since Scala is now required anyway for Isabelle

diff -r 264ece81df93 -r 1ea90e8046dc src/HOL/Imperative_HOL/Imperative_HOL_ex.thy
--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Fri Dec 28 10:15:39 2012 +0100
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Fri Dec 28 10:25:59 2012 +0100
@@ -14,6 +14,6 @@
   Array.upd, Array.map_entry, Array.swap, Array.freeze,
   ref, Ref.lookup, Ref.update, Ref.change)"
 
-export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
+export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
 
 end
diff -r 264ece81df93 -r 1ea90e8046dc src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Dec 28 10:15:39 2012 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Dec 28 10:25:59 2012 +0100
@@ -659,6 +659,6 @@
 
 ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
 
-export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
+export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
 
 end
diff -r 264ece81df93 -r 1ea90e8046dc src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Fri Dec 28 10:15:39 2012 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Fri Dec 28 10:25:59 2012 +0100
@@ -112,7 +112,7 @@
 
 definition "example = (Array.make 10 id \<guillemotright>= (\<lambda>a. rev a 0 9))"
 
-export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
+export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
 
 end
 
diff -r 264ece81df93 -r 1ea90e8046dc src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Dec 28 10:15:39 2012 +0100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Dec 28 10:25:59 2012 +0100
@@ -1000,7 +1000,7 @@
 ML {* @{code test_2} () *}
 ML {* @{code test_3} () *}
 
-export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
+export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
 
 end