drop workaround addressed by d0d3c30806b4
authorAndreas Lochbihler
Mon Sep 22 10:53:54 2014 +0200 (2014-09-22)
changeset 58414f945e7af0d27
parent 58413 22dd971f6938
child 58416 d94ec306b7a8
drop workaround addressed by d0d3c30806b4
src/HOL/Codegenerator_Test/Code_Test_GHC.thy
     1.1 --- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Sun Sep 21 20:22:12 2014 +0200
     1.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Mon Sep 22 10:53:54 2014 +0200
     1.3 @@ -6,9 +6,7 @@
     1.4  
     1.5  theory Code_Test_GHC imports Code_Test begin
     1.6  
     1.7 -definition id_integer :: "integer \<Rightarrow> integer" where "id_integer = id"
     1.8 -
     1.9 -test_code "id_integer (14 + 7 * -12) = 140 div -2" in GHC
    1.10 +test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC
    1.11  
    1.12  value [GHC] "14 + 7 * -12 :: integer"
    1.13