# HG changeset patch
# User haftmann
# Date 1167242995 -3600
# Node ID db805c70a5194fc27f2d8ccb3e18749d47ea146f
# Parent  500f91bf992c84e28b849f754a31a17cd635217a
explizit serialization for Haskell id

diff -r 500f91bf992c -r db805c70a519 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Wed Dec 27 19:09:54 2006 +0100
+++ b/src/HOL/Fun.thy	Wed Dec 27 19:09:55 2006 +0100
@@ -480,6 +480,9 @@
   (SML infixl 5 "o")
   (Haskell infixr 9 ".")
 
+code_const "id"
+  (Haskell "id")
+
 
 subsection {* ML legacy bindings *}