# HG changeset patch
# User haftmann
# Date 1159822856 -7200
# Node ID e115ea078a30f420a2099abd5844af13f65c0b9d
# Parent  099877d83d2b5cdb72d527d2c8a0dca6e4ebab33
cleaned mess

diff -r 099877d83d2b -r e115ea078a30 src/HOL/Lambda/WeakNorm.thy
--- 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"