# HG changeset patch
# User haftmann
# Date 1149598929 -7200
# Node ID 1c788c6974e8b962dc8fecdb70fcf7ffcd7f201e
# Parent  c08c9f9ea9a5825e6ee06c1f15c14bfbe5b303ba
added arbitray setup for codegen 2

diff -r c08c9f9ea9a5 -r 1c788c6974e8 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Tue Jun 06 15:01:09 2006 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Tue Jun 06 15:02:09 2006 +0200
@@ -501,6 +501,10 @@
   arbitrary :: "'a"       ("(error \"arbitrary\")")
   arbitrary :: "'a \<Rightarrow> 'b" ("(fn '_ => error \"arbitrary\")")
 
+code_syntax_const
+  "arbitrary :: 'a"       ml (target_atom "(error \"arbitrary\")")
+  "arbitrary :: 'a \<Rightarrow> 'b" ml (target_atom "(fn '_ => error \"arbitrary\")")
+
 code_module Norm
 contains
   test = "type_NF"