avoid export_code ... file -

--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Wed Jul 14 16:02:50 2010 +0200
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Wed Jul 14 16:13:14 2010 +0200
@@ -10,4 +10,6 @@
   "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" "ex/SatChecker"
 begin
 
+export_code "Array.*" "Ref.*" checking SML SML_imp OCaml? OCaml_imp? Haskell?
+
 end

--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Wed Jul 14 16:02:50 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Wed Jul 14 16:13:14 2010 +0200
@@ -655,9 +655,6 @@
 
 ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
 
-export_code qsort in SML_imp module_name QSort file -
-export_code qsort in OCaml module_name QSort file -
-export_code qsort in OCaml_imp module_name QSort file -
-export_code qsort in Haskell module_name QSort file -
+export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell?
 
 end
\ No newline at end of file

--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Wed Jul 14 16:02:50 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Wed Jul 14 16:13:14 2010 +0200
@@ -110,4 +110,6 @@
       subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
   (drule sym[of "List.length (Array.get h a)"], simp)
 
+export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell?
+
 end

--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Wed Jul 14 16:02:50 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Wed Jul 14 16:13:14 2010 +0200
@@ -991,10 +991,6 @@
 
 section {* Code generation *}
 
-export_code merge in SML file -
-
-export_code rev in SML file -
-
 text {* A simple example program *}
 
 definition test_1 where "test_1 = (do { ll_xs <- make_llist [1..(15::int)]; xs <- traverse ll_xs; return xs })" 
@@ -1018,9 +1014,6 @@
 ML {* @{code test_2} () *}
 ML {* @{code test_3} () *}
 
-export_code test_1 test_2 test_3 in SML_imp module_name QSort file -
-export_code test_1 test_2 test_3 in OCaml module_name QSort file -
-export_code test_1 test_2 test_3 in OCaml_imp module_name QSort file -
-export_code test_1 test_2 test_3 in Haskell module_name QSort file -
+export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell?
 
 end

--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Wed Jul 14 16:02:50 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Wed Jul 14 16:13:14 2010 +0200
@@ -710,8 +710,6 @@
 code_const ProofDone  and  Root              and  Conflict              and  Delete  and  Xstep
      (SML "MinisatProofStep.ProofDone" and "MinisatProofStep.Root ((_),/ (_))" and "MinisatProofStep.Conflict ((_),/ (_))" and "MinisatProofStep.Delete" and "MinisatProofStep.Xstep ((_),/ (_))")
 
-export_code checker in SML module_name SAT file -
-export_code tchecker in SML module_name SAT file -
-export_code lchecker in SML module_name SAT file -
+export_code checker tchecker lchecker in SML
 
 end

--- a/src/HOL/ex/Numeral.thy	Wed Jul 14 16:02:50 2010 +0200
+++ b/src/HOL/ex/Numeral.thy	Wed Jul 14 16:13:14 2010 +0200
@@ -988,9 +988,9 @@
 subsection {* Toy examples *}
 
 definition "bar \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat) \<and> #4 * #2 + #7 \<ge> (#8 :: int) - #3"
+
 code_thms bar
-export_code bar in Haskell file -
-export_code bar in OCaml module_name Foo file -
-ML {* @{code bar} *}
+
+export_code bar checking SML OCaml? Haskell?
 
 end

--- a/src/HOL/ex/Records.thy	Wed Jul 14 16:02:50 2010 +0200
+++ b/src/HOL/ex/Records.thy	Wed Jul 14 16:13:14 2010 +0200
@@ -346,6 +346,6 @@
 
 subsection {* Some code generation *}
 
-export_code foo1 foo3 foo5 foo10 foo11 in SML file -
+export_code foo1 foo3 foo5 foo10 checking SML
 
 end