cleaned mess

--- a/src/HOL/Lambda/WeakNorm.thy	Mon Oct 02 23:00:53 2006 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Mon Oct 02 23:00:56 2006 +0200
@@ -501,10 +501,6 @@
   arbitrary :: "'a"       ("(error \"arbitrary\")")
   arbitrary :: "'a \<Rightarrow> 'b" ("(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
   test = "type_NF"