diff -r ebde66a71ab0 -r cdff6ef76009 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Wed May 09 07:53:04 2007 +0200
+++ b/src/HOL/Fun.thy	Wed May 09 07:53:06 2007 +0200
@@ -7,12 +7,12 @@
 header {* Notions about functions *}
 
 theory Fun
-imports Set Code_Generator
+imports Set
 begin
 
 constdefs
   fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)"
-  [code func]: "fun_upd f a b == % x. if x=a then b else f x"
+  "fun_upd f a b == % x. if x=a then b else f x"
 
 nonterminals
   updbinds updbind