--- a/src/HOL/Lambda/WeakNorm.thy Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Fri Sep 01 08:36:51 2006 +0200
@@ -501,9 +501,9 @@
arbitrary :: "'a" ("(error \"arbitrary\")")
arbitrary :: "'a \<Rightarrow> 'b" ("(fn '_ => error \"arbitrary\")")
-code_constapp
- "arbitrary :: 'a" ml (target_atom "(error \"arbitrary\")")
- "arbitrary :: 'a \<Rightarrow> 'b" ml (target_atom "(fn '_ => error \"arbitrary\")")
+code_const "arbitrary :: 'a" and "arbitrary :: 'a \<Rightarrow> 'b"
+ (SML target_atom "(error \"arbitrary\")"
+ and target_atom "(fn '_ => error \"arbitrary\")")
code_module Norm
contains