diff -r 5ac79735cfef -r e4640c2ceb43 src/HOL/Imperative_HOL/ex/Linked_Lists.thy --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Thu Jul 29 09:56:59 2010 +0200 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Thu Jul 29 09:56:59 2010 +0200 @@ -1014,6 +1014,6 @@ 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? +export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? (*Scala_imp?*) end