# HG changeset patch
# User Andreas Lochbihler
# Date 1411376034 -7200
# Node ID f945e7af0d277fb4e5d9f2d01fdd50205d968297
# Parent  22dd971f6938bfd00dce20951f8bd3b70896c0f2
drop workaround addressed by d0d3c30806b4

diff -r 22dd971f6938 -r f945e7af0d27 src/HOL/Codegenerator_Test/Code_Test_GHC.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Sun Sep 21 20:22:12 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Mon Sep 22 10:53:54 2014 +0200
@@ -6,9 +6,7 @@
 
 theory Code_Test_GHC imports Code_Test begin
 
-definition id_integer :: "integer \<Rightarrow> integer" where "id_integer = id"
-
-test_code "id_integer (14 + 7 * -12) = 140 div -2" in GHC
+test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC
 
 value [GHC] "14 + 7 * -12 :: integer"