diff -r 101aefd61aac -r 747d716e98d0 src/HOL/Code_Generator.thy --- a/src/HOL/Code_Generator.thy Fri Oct 20 17:07:26 2006 +0200 +++ b/src/HOL/Code_Generator.thy Fri Oct 20 17:07:27 2006 +0200 @@ -106,6 +106,8 @@ code_const arbitrary (Haskell target_atom "(error \"arbitrary\")") +code_reserved SML Fail +code_reserved Haskell error subsection {* Operational equality for code generation *} @@ -169,6 +171,8 @@ code_const "eq \ bool \ bool \ bool" (Haskell infixl 4 "==") +code_reserved Haskell + Eq eq subsection {* normalization by evaluation *}