added arbitray setup for codegen 2
authorhaftmann
Tue, 06 Jun 2006 15:02:09 +0200
changeset 19790 1c788c6974e8
parent 19789 c08c9f9ea9a5
child 19791 ab326de16ad5
added arbitray setup for codegen 2
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"