1.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Thu Jul 29 12:07:09 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Thu Jul 29 15:07:52 2010 +0200
     1.3 @@ -263,22 +263,32 @@
     1.4  
     1.5  subsection {* Code generator setup *}
     1.6  
     1.7 +text {* Intermediate operation avoids invariance problem in @{text Scala} (similiar to value restriction) *}
     1.8 +
     1.9 +definition ref' where
    1.10 +  [code del]: "ref' = ref"
    1.11 +
    1.12 +lemma [code]:
    1.13 +  "ref x = ref' x"
    1.14 +  by (simp add: ref'_def)
    1.15 +
    1.16 +
    1.17  text {* SML *}
    1.18  
    1.19  code_type ref (SML "_/ Unsynchronized.ref")
    1.20  code_const Ref (SML "raise/ (Fail/ \"bare Ref\")")
    1.21 -code_const ref (SML "(fn/ ()/ =>/ Unsynchronized.ref/ _)")
    1.22 +code_const ref' (SML "(fn/ ()/ =>/ Unsynchronized.ref/ _)")
    1.23  code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)")
    1.24  code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)")
    1.25  
    1.26 -code_reserved SML ref
    1.27 +code_reserved SML Unsynchronized
    1.28  
    1.29  
    1.30  text {* OCaml *}
    1.31  
    1.32  code_type ref (OCaml "_/ ref")
    1.33  code_const Ref (OCaml "failwith/ \"bare Ref\"")
    1.34 -code_const ref (OCaml "(fun/ ()/ ->/ ref/ _)")
    1.35 +code_const ref' (OCaml "(fun/ ()/ ->/ ref/ _)")
    1.36  code_const Ref.lookup (OCaml "(fun/ ()/ ->/ !/ _)")
    1.37  code_const Ref.update (OCaml "(fun/ ()/ ->/ _/ :=/ _)")
    1.38  
    1.39 @@ -289,7 +299,7 @@
    1.40  
    1.41  code_type ref (Haskell "Heap.STRef/ Heap.RealWorld/ _")
    1.42  code_const Ref (Haskell "error/ \"bare Ref\"")
    1.43 -code_const ref (Haskell "Heap.newSTRef")
    1.44 +code_const ref' (Haskell "Heap.newSTRef")
    1.45  code_const Ref.lookup (Haskell "Heap.readSTRef")
    1.46  code_const Ref.update (Haskell "Heap.writeSTRef")
    1.47  
    1.48 @@ -298,7 +308,7 @@
    1.49  
    1.50  code_type ref (Scala "!Ref[_]")
    1.51  code_const Ref (Scala "!error(\"bare Ref\")")
    1.52 -code_const ref (Scala "('_: Unit)/ =>/ Ref((_))")
    1.53 +code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
    1.54  code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
    1.55  code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
    1.56  

     2.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Thu Jul 29 12:07:09 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Thu Jul 29 15:07:52 2010 +0200
     2.3 @@ -110,7 +110,7 @@
     2.4        subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
     2.5    (drule sym[of "List.length (Array.get h a)"], simp)
     2.6  
     2.7 -definition "example = (Array.of_list [1::nat, 2, 3, 4, 5, 6, 7, 8, 9, 10] \<guillemotright>= (\<lambda>a. rev a 0 9))"
     2.8 +definition "example = (Array.make 10 id \<guillemotright>= (\<lambda>a. rev a 0 9))"
     2.9  
    2.10  export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
    2.11  

     3.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Thu Jul 29 12:07:09 2010 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Thu Jul 29 15:07:52 2010 +0200
     3.3 @@ -1014,6 +1014,6 @@
     3.4  ML {* @{code test_2} () *}
     3.5  ML {* @{code test_3} () *}
     3.6  
     3.7 -export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? (*Scala_imp?*)
     3.8 +export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
     3.9  
    3.10  end

     4.1 --- a/src/Tools/Code/code_ml.ML	Thu Jul 29 12:07:09 2010 +0200
     4.2 +++ b/src/Tools/Code/code_ml.ML	Thu Jul 29 15:07:52 2010 +0200
     4.3 @@ -987,7 +987,8 @@
     4.4        )))
     4.5    #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
     4.6    #> fold (Code_Target.add_reserved target_SML)
     4.7 -      ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*), "IntInf"]
     4.8 +      ["ref" (*rebinding is illegal*), "o" (*dictionary projections use it already*),
     4.9 +        "Fail", "div", "mod" (*standard infixes*), "IntInf"]
    4.10    #> fold (Code_Target.add_reserved target_OCaml) [
    4.11        "and", "as", "assert", "begin", "class",
    4.12        "constraint", "do", "done", "downto", "else", "end", "exception",