# HG changeset patch
# User krauss
# Date 1164372224 -3600
# Node ID 16c62deb1adfac23edfa0b5c99835e3cffdeb0b3
# Parent  7e72185e4b242a43df37a8b082b10de7d20b7724
The function package declares the [code] attribute automatically again.

diff -r 7e72185e4b24 -r 16c62deb1adf src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Fri Nov 24 13:39:22 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Fri Nov 24 13:43:44 2006 +0100
@@ -125,7 +125,6 @@
 termination by lexicographic_order
 
 lemmas unionl_def = unionl.simps(2)
-declare unionl.simps[code]
 
 function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
@@ -136,7 +135,6 @@
 termination by lexicographic_order
 
 lemmas intersect_def = intersect.simps(3)
-declare intersect.simps[code]
 
 function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
@@ -147,7 +145,6 @@
 termination by lexicographic_order
 
 lemmas subtract_def = subtract.simps(3)
-declare subtract.simps[code]
 
 function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
 where
@@ -157,7 +154,6 @@
 termination by lexicographic_order
 
 lemmas map_distinct_def = map_distinct.simps(2)
-declare map_distinct.simps[code]
 
 function unions :: "'a list list \<Rightarrow> 'a list"
 where
@@ -167,7 +163,6 @@
 termination by lexicographic_order
 
 lemmas unions_def = unions.simps(2)
-declare unions.simps[code]
 
 consts intersects :: "'a list list \<Rightarrow> 'a list"
 primrec
diff -r 7e72185e4b24 -r 16c62deb1adf src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Nov 24 13:39:22 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Nov 24 13:43:44 2006 +0100
@@ -142,15 +142,15 @@
       val tsimps = PROFILE "making tsimps" (map remove_domain_condition) psimps
       val tinduct = PROFILE "making tinduct" (map remove_domain_condition) pinducts
 
-        (* FIXME: How to generate code from (possibly) local contexts
-        val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
-        val allatts = if has_guards then [] else [Attrib.internal (RecfunCodegen.add NONE)]
-        *)
-        val qualify = NameSpace.qualified defname;
+        (* FIXME: How to generate code from (possibly) local contexts*)
+      val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
+      val allatts = if has_guards then [] else [Attrib.internal (RecfunCodegen.add NONE)]
+        
+      val qualify = NameSpace.qualified defname;
     in
-        lthy
-          |> PROFILE "adding tsimps" (add_simps "simps" [] mutual fixes tsimps spec) |> snd
-          |> PROFILE "adding tinduct" (note_theorem ((qualify "induct", []), tinduct)) |> snd
+      lthy
+        |> PROFILE "adding tsimps" (add_simps "simps" allatts mutual fixes tsimps spec) |> snd
+        |> PROFILE "adding tinduct" (note_theorem ((qualify "induct", []), tinduct)) |> snd
     end
 
 
diff -r 7e72185e4b24 -r 16c62deb1adf src/HOL/ex/Codegenerator.thy
--- a/src/HOL/ex/Codegenerator.thy	Fri Nov 24 13:39:22 2006 +0100
+++ b/src/HOL/ex/Codegenerator.thy	Fri Nov 24 13:43:44 2006 +0100
@@ -54,8 +54,6 @@
   by pat_completeness auto
 termination by (relation "measure nat") auto
 
-declare fac.simps [code]
-
 subsection {* sums *}
 
 subsection {* options *}