changeset 20838 | e115ea078a30 |
parent 20713 | 823967ef47f1 |
child 20942 | 43e216a9d615 |
--- 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"