# HG changeset patch
# User haftmann
# Date 1177060902 -7200
# Node ID 5cbe966d67a2196a2c53fbf8ac0cf78437de141e
# Parent  e2b06bfe471a16d3471b37b7a0bcaf8f50fdd94c
Isar definitions are now added explicitly to code theorem table

diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Code_Generator.thy
--- a/src/HOL/Code_Generator.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Code_Generator.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -219,7 +219,7 @@
 
 definition
   if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a" where
-  "if_delayed b f g = (if b then f True else g False)"
+  [code nofunc]: "if_delayed b f g = (if b then f True else g False)"
 
 lemma [code func]:
   shows "if_delayed True f g = f True"
@@ -230,7 +230,6 @@
   "(if b then x else y) = if_delayed b (\<lambda>_. x) (\<lambda>_. y)"
   unfolding if_delayed_def ..
 
-
 hide (open) const if_delayed
 
 end
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Datatype.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -102,7 +102,7 @@
 
 (** apfst -- can be used in similar type definitions **)
 
-lemma apfst_conv [simp]: "apfst f (a,b) = (f(a),b)"
+lemma apfst_conv [simp, code func]: "apfst f (a, b) = (f a, b)"
 by (simp add: apfst_def)
 
 
@@ -697,10 +697,10 @@
   option_map :: "('a => 'b) => ('a option => 'b option)"
   "option_map == %f y. case y of None => None | Some x => Some (f x)"
 
-lemma option_map_None [simp]: "option_map f None = None"
+lemma option_map_None [simp, code func]: "option_map f None = None"
   by (simp add: option_map_def)
 
-lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)"
+lemma option_map_Some [simp, code func]: "option_map f (Some x) = Some (f x)"
   by (simp add: option_map_def)
 
 lemma option_map_is_None [iff]:
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Divides.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -871,9 +871,9 @@
   done
 
 
-subsection {* Code generation for div and mod *}
+subsection {* Code generation for div, mod and dvd on nat *}
 
-definition
+definition [code nofunc]:
   "divmod (m\<Colon>nat) n = (m div n, m mod n)"
 
 lemma divmod_zero [code]: "divmod m 0 = (0, m)"
@@ -893,13 +893,22 @@
 lemma mod_divmod [code]: "m mod n = snd (divmod m n)"
   unfolding divmod_def by simp
 
+definition
+  dvd_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
+where
+  "dvd_nat m n \<longleftrightarrow> n mod m = (0 \<Colon> nat)"
+
+lemma [code inline]:
+  "op dvd = dvd_nat"
+  by (auto simp add: dvd_nat_def dvd_eq_mod_eq_0 expand_fun_eq)
+
 code_modulename SML
   Divides Integer
 
 code_modulename OCaml
   Divides Integer
 
-hide (open) const divmod
+hide (open) const divmod dvd_nat
 
 subsection {* Legacy bindings *}
 
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/FixedPoint.thy
--- a/src/HOL/FixedPoint.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/FixedPoint.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -198,6 +198,8 @@
   apply (iprover elim: le_funE)
   done
 
+lemmas [code nofunc] = Inf_fun_def
+
 theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})"
   apply (rule order_antisym)
   apply (rule Sup_least)
@@ -219,6 +221,8 @@
   Inf_set_def: "Inf S \<equiv> \<Inter>S"
   by intro_classes (auto simp add: Inf_set_def)
 
+lemmas [code nofunc] = Inf_set_def
+
 theorem Sup_set_eq: "Sup S = \<Union>S"
   apply (rule subset_antisym)
   apply (rule Sup_least)
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Fun.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -12,7 +12,7 @@
 
 constdefs
   fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)"
-   "fun_upd f a b == % x. if x=a then b else f x"
+  [code func]: "fun_upd f a b == % x. if x=a then b else f x"
 
 nonterminals
   updbinds updbind
@@ -34,15 +34,20 @@
  "fun_sum" == sum_case
 *)
 
-constdefs
-  override_on :: "('a => 'b) => ('a => 'b) => 'a set => ('a => 'b)"
-  "override_on f g A == %a. if a : A then g a else f a"
+definition
+  override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b"
+where
+  "override_on f g A = (\<lambda>a. if a \<in> A then g a else f a)"
 
-  id :: "'a => 'a"
-  "id == %x. x"
+definition
+  id :: "'a \<Rightarrow> 'a"
+where
+  "id = (\<lambda>x. x)"
 
-  comp :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixl "o" 55)
-  "f o g == %x. f(g(x))"
+definition
+  comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o" 55)
+where
+  "f o g = (\<lambda>x. f (g x))"
 
 notation (xsymbols)
   comp  (infixl "\<circ>" 55)
@@ -404,9 +409,10 @@
 
 subsection{* swap *}
 
-constdefs
-  swap :: "['a, 'a, 'a => 'b] => ('a => 'b)"
-   "swap a b f == f(a := f b, b:= f a)"
+definition
+  swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
+where
+  "swap a b f = f (a := f b, b:= f a)"
 
 lemma swap_self: "swap a a f = f"
 by (simp add: swap_def)
@@ -418,7 +424,7 @@
 by (rule ext, simp add: fun_upd_def swap_def)
 
 lemma inj_on_imp_inj_on_swap:
-     "[|inj_on f A; a \<in> A; b \<in> A|] ==> inj_on (swap a b f) A"
+  "[|inj_on f A; a \<in> A; b \<in> A|] ==> inj_on (swap a b f) A"
 by (simp add: inj_on_def swap_def, blast)
 
 lemma inj_on_swap_iff [simp]:
@@ -460,6 +466,8 @@
   le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x"
   less_fun_def: "f < g \<equiv> f \<le> g \<and> f \<noteq> g" ..
 
+lemmas [code nofunc] = le_fun_def less_fun_def
+
 instance "fun" :: (type, preorder) preorder
   by default (auto simp add: le_fun_def less_fun_def intro: order_trans)
 
@@ -528,6 +536,8 @@
 apply (auto dest: le_funD)
 done
 
+lemmas [code nofunc] = inf_fun_eq sup_fun_eq
+
 instance "fun" :: (type, distrib_lattice) distrib_lattice
   by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
 
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/HOL.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -165,7 +165,7 @@
   True_or_False:  "(P=True) | (P=False)"
 
 defs
-  Let_def:      "Let s f == f(s)"
+  Let_def [code func]: "Let s f == f(s)"
   if_def:       "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)"
 
 finalconsts
@@ -177,7 +177,7 @@
 axiomatization
   undefined :: 'a
 
-axioms
+axiomatization where
   undefined_fun: "undefined x = undefined"
 
 
@@ -912,8 +912,8 @@
 structure Blast = BlastFun(
 struct
   type claset = Classical.claset
-  val equality_name = "op ="
-  val not_name = "Not"
+  val equality_name = @{const_name "op ="}
+  val not_name = @{const_name "Not"}
   val notE = @{thm HOL.notE}
   val ccontr = @{thm HOL.ccontr}
   val contr_tac = Classical.contr_tac
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Integ/IntDef.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -517,15 +517,16 @@
 
 subsection{*The Constants @{term neg} and @{term iszero}*}
 
-constdefs
-
-  neg   :: "'a::ordered_idom => bool"
-  "neg(Z) == Z < 0"
+definition
+  neg  :: "'a\<Colon>ordered_idom \<Rightarrow> bool"
+where
+  "neg Z \<longleftrightarrow> Z < 0"
 
+definition
   (*For simplifying equalities*)
-  iszero :: "'a::comm_semiring_1_cancel => bool"
-  "iszero z == z = (0)"
-
+  iszero :: "'a\<Colon>comm_semiring_1_cancel \<Rightarrow> bool"
+where
+  "iszero z \<longleftrightarrow> z = 0"
 
 lemma not_neg_int [simp]: "~ neg(int n)"
 by (simp add: neg_def)
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Integ/IntDiv.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -18,13 +18,13 @@
 constdefs
   quorem :: "(int*int) * (int*int) => bool"
     --{*definition of quotient and remainder*}
-    "quorem == %((a,b), (q,r)).
+    [code func]: "quorem == %((a,b), (q,r)).
                       a = b*q + r &
                       (if 0 < b then 0\<le>r & r<b else b<r & r \<le> 0)"
 
   adjust :: "[int, int*int] => int*int"
     --{*for the division algorithm*}
-    "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
+    [code func]: "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
                          else (2*q, r)"
 
 text{*algorithm for the case @{text "a\<ge>0, b>0"}*}
@@ -44,13 +44,13 @@
 text{*algorithm for the general case @{term "b\<noteq>0"}*}
 constdefs
   negateSnd :: "int*int => int*int"
-    "negateSnd == %(q,r). (q,-r)"
+    [code func]: "negateSnd == %(q,r). (q,-r)"
 
   divAlg :: "int*int => int*int"
     --{*The full division algorithm considers all possible signs for a, b
        including the special case @{text "a=0, b<0"} because 
        @{term negDivAlg} requires @{term "a<0"}.*}
-    "divAlg ==
+    [code func]: "divAlg ==
        %(a,b). if 0\<le>a then
                   if 0\<le>b then posDivAlg (a,b)
                   else if a=0 then (0,0)
@@ -65,8 +65,8 @@
 text{*The operators are defined with reference to the algorithm, which is
 proved to satisfy the specification.*}
 defs
-  div_def:   "a div b == fst (divAlg (a,b))"
-  mod_def:   "a mod b == snd (divAlg (a,b))"
+  div_def [code func]: "a div b == fst (divAlg (a,b))"
+  mod_def [code func]: "a mod b == snd (divAlg (a,b))"
 
 
 text{*
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Integ/Numeral.thy
--- a/src/HOL/Integ/Numeral.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Integ/Numeral.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -32,15 +32,15 @@
 
 definition
   Pls :: int where
-  "Pls = 0"
+  [code nofunc]:"Pls = 0"
 
 definition
   Min :: int where
-  "Min = - 1"
+  [code nofunc]:"Min = - 1"
 
 definition
   Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
-  "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
+  [code nofunc]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
 
 class number = type + -- {* for numeric types: nat, int, real, \dots *}
   fixes number_of :: "int \<Rightarrow> 'a"
@@ -68,11 +68,11 @@
 
 definition
   succ :: "int \<Rightarrow> int" where
-  "succ k = k + 1"
+  [code nofunc]: "succ k = k + 1"
 
 definition
   pred :: "int \<Rightarrow> int" where
-  "pred k = k - 1"
+  [code nofunc]: "pred k = k - 1"
 
 declare
  max_def[of "number_of u" "number_of v", standard, simp]
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Integ/Presburger.thy
--- a/src/HOL/Integ/Presburger.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Integ/Presburger.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -1069,11 +1069,12 @@
 lemma eq_number_of [code func]:
   "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
   unfolding number_of_is_id ..
+
 lemma eq_Pls_Pls:
-  "Numeral.Pls = Numeral.Pls" ..
+  "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by rule+
 
 lemma eq_Pls_Min:
-  "Numeral.Pls \<noteq> Numeral.Min"
+  "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
   unfolding Pls_def Min_def by auto
 
 lemma eq_Pls_Bit0:
@@ -1081,18 +1082,18 @@
   unfolding Pls_def Bit_def bit.cases by auto
 
 lemma eq_Pls_Bit1:
-  "Numeral.Pls \<noteq> Numeral.Bit k bit.B1"
+  "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
   unfolding Pls_def Bit_def bit.cases by arith
 
 lemma eq_Min_Pls:
-  "Numeral.Min \<noteq> Numeral.Pls"
+  "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
   unfolding Pls_def Min_def by auto
 
 lemma eq_Min_Min:
-  "Numeral.Min = Numeral.Min" ..
+  "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by rule+
 
 lemma eq_Min_Bit0:
-  "Numeral.Min \<noteq> Numeral.Bit k bit.B0"
+  "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
   unfolding Min_def Bit_def bit.cases by arith
 
 lemma eq_Min_Bit1:
@@ -1104,11 +1105,11 @@
   unfolding Pls_def Bit_def bit.cases by auto
 
 lemma eq_Bit1_Pls:
-  "Numeral.Bit k bit.B1 \<noteq>  Numeral.Pls"
+  "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
   unfolding Pls_def Bit_def bit.cases by arith
 
 lemma eq_Bit0_Min:
-  "Numeral.Bit k bit.B0 \<noteq> Numeral.Min"
+  "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
   unfolding Min_def Bit_def bit.cases by arith
 
 lemma eq_Bit1_Min:
@@ -1140,10 +1141,10 @@
   unfolding number_of_is_id ..
 
 lemma less_eq_Pls_Pls:
-  "Numeral.Pls \<le> Numeral.Pls" ..
+  "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
 
 lemma less_eq_Pls_Min:
-  "\<not> (Numeral.Pls \<le> Numeral.Min)"
+  "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
   unfolding Pls_def Min_def by auto
 
 lemma less_eq_Pls_Bit:
@@ -1151,11 +1152,11 @@
   unfolding Pls_def Bit_def by (cases v) auto
 
 lemma less_eq_Min_Pls:
-  "Numeral.Min \<le> Numeral.Pls"
+  "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
   unfolding Pls_def Min_def by auto
 
 lemma less_eq_Min_Min:
-  "Numeral.Min \<le> Numeral.Min" ..
+  "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
 
 lemma less_eq_Min_Bit0:
   "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
@@ -1198,10 +1199,10 @@
   unfolding number_of_is_id ..
 
 lemma less_Pls_Pls:
-  "\<not> (Numeral.Pls < Numeral.Pls)" by auto
+  "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by auto
 
 lemma less_Pls_Min:
-  "\<not> (Numeral.Pls < Numeral.Min)"
+  "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
   unfolding Pls_def Min_def by auto
 
 lemma less_Pls_Bit0:
@@ -1213,11 +1214,11 @@
   unfolding Pls_def Bit_def by auto
 
 lemma less_Min_Pls:
-  "Numeral.Min < Numeral.Pls"
+  "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
   unfolding Pls_def Min_def by auto
 
 lemma less_Min_Min:
-  "\<not> (Numeral.Min < Numeral.Min)" by auto
+  "Numeral.Min < Numeral.Min \<longleftrightarrow> False" by auto
 
 lemma less_Min_Bit:
   "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Library/ExecutableSet.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -287,6 +287,12 @@
   "image (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq) = image f" ..
 
 lemma [code func]:
+  "Union (xss \<Colon> 'a\<Colon>eq set set) = Union xss" ..
+
+lemma [code func]:
+  "Inter (xss \<Colon> 'a\<Colon>eq set set) = Inter xss" ..
+
+lemma [code func]:
   "UNION xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = UNION xs f" ..
 
 lemma [code func]:
@@ -301,6 +307,7 @@
 lemma [code func]:
   "filter_set P (xs \<Colon> 'a\<Colon>type set) = filter_set P xs" ..
 
+
 code_abstype "'a set" "'a list" where
   "{}" \<equiv> empty_list
   insert \<equiv> insertl
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Library/Graphs.thy
--- a/src/HOL/Library/Graphs.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Library/Graphs.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -73,13 +73,14 @@
   by auto
 qed
 
+lemmas [code nofunc] = graph_plus_def
 
 instance graph :: (type, type) "{distrib_lattice, complete_lattice}"
   graph_leq_def: "G \<le> H \<equiv> dest_graph G \<subseteq> dest_graph H"
   graph_less_def: "G < H \<equiv> dest_graph G \<subset> dest_graph H"
   "inf G H \<equiv> Graph (dest_graph G \<inter> dest_graph H)"
   "sup G H \<equiv> G + H"
-  Inf_graph_def: "Inf == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
+  Inf_graph_def: "Inf \<equiv> \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
 proof
   fix x y z :: "('a,'b) graph"
   fix A :: "('a, 'b) graph set"
@@ -122,6 +123,9 @@
     unfolding Inf_graph_def graph_leq_def by auto }
 qed
 
+lemmas [code nofunc] = graph_leq_def graph_less_def
+  inf_graph_def sup_graph_def Inf_graph_def
+
 lemma in_grplus:
   "has_edge (G + H) p b q = (has_edge G p b q \<or> has_edge H p b q)"
   by (cases G, cases H, auto simp:has_edge_def graph_plus_def)
@@ -146,6 +150,8 @@
     by (cases a) (simp add:grcomp.simps)
 qed
 
+lemmas [code nofunc] = graph_mult_def
+
 instance graph :: (type, one) one 
   graph_one_def: "1 == Graph { (x, 1, x) |x. True}" ..
 
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Library/List_lexord.thy
--- a/src/HOL/Library/List_lexord.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Library/List_lexord.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -13,7 +13,7 @@
   list_le_def:  "(xs::('a::ord) list) \<le> ys \<equiv> (xs < ys \<or> xs = ys)"
   list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> lexord {(u,v). u < v}" ..
 
-lemmas list_ord_defs = list_less_def list_le_def
+lemmas list_ord_defs [code nofunc] = list_less_def list_le_def
 
 instance list :: (order) order
   apply (intro_classes, unfold list_ord_defs)
@@ -40,6 +40,8 @@
   by intro_classes
     (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
 
+lemmas [code nofunc] = inf_list_def sup_list_def
+
 lemma not_less_Nil [simp]: "\<not> (x < [])"
   by (unfold list_less_def) simp
 
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Library/Product_ord.thy
--- a/src/HOL/Library/Product_ord.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Library/Product_ord.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -13,7 +13,7 @@
   prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x \<le> snd y)"
   prod_less_def: "(x < y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x < snd y)" ..
 
-lemmas prod_ord_defs = prod_less_def prod_le_def
+lemmas prod_ord_defs [code nofunc] = prod_less_def prod_le_def
 
 lemma [code func]:
   "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Library/SCT_Definition.thy
--- a/src/HOL/Library/SCT_Definition.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Library/SCT_Definition.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -15,12 +15,11 @@
     LESS ("\<down>")
   | LEQ ("\<Down>")
 
-instance sedge :: times ..
-instance sedge :: one ..
+instance sedge :: one
+  one_sedge_def: "1 \<equiv> \<Down>" ..
 
-defs (overloaded)
-  one_sedge_def: "1 == \<Down>"
-  mult_sedge_def:" a * b == (if a = \<down> then \<down> else b)"
+instance sedge :: times
+  mult_sedge_def:" a * b \<equiv> if a = \<down> then \<down> else b" ..
 
 instance sedge :: comm_monoid_mult
 proof
@@ -31,14 +30,18 @@
     by (cases a, simp) (cases b, auto)
 qed
 
+lemma sedge_UNIV:
+  "UNIV = { LESS, LEQ }"
+  by auto (case_tac x, auto) (*FIXME*)
+
 instance sedge :: finite
 proof
-  have a: "UNIV = { LESS, LEQ }"
-    by auto (case_tac x, auto) (* FIXME *)
   show "finite (UNIV::sedge set)"
-    by (simp add:a)
+    by (simp add: sedge_UNIV)
 qed
 
+lemmas [code func] = sedge_UNIV
+
 
 types scg = "(nat, sedge) graph"
 types acg = "(nat, scg) graph"
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Library/SCT_Implementation.thy
--- a/src/HOL/Library/SCT_Implementation.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Library/SCT_Implementation.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -19,11 +19,10 @@
 where
   "connect_edges ((n,e,m), (n', e', m')) = (n, e * e', m')"
 
-lemma grcomp_code[code]:
+lemma grcomp_code [code]:
   "grcomp (Graph G) (Graph H) = Graph (connect_edges ` { x \<in> G\<times>H. edges_match x })"
   by (rule graph_ext) (auto simp:graph_mult_def has_edge_def image_def)
 
-
 definition test_SCT :: "acg \<Rightarrow> bool"
 where
   "test_SCT \<A> = 
@@ -119,6 +118,6 @@
   Kleene_Algebras SCT
   SCT_Implementation SCT
 
-code_gen test_SCT (SML -)
+code_gen test_SCT (SML #)
 
 end
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Map.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -84,7 +84,7 @@
   "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
 
 defs
-  map_upds_def: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
+  map_upds_def [code func]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
 
 
 subsection {* @{term [source] empty} *}
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Nat.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -62,7 +62,9 @@
   Zero_nat_def: "0 == Abs_Nat Zero_Rep"
   One_nat_def [simp]: "1 == Suc 0"
   less_def: "m < n == (m, n) : pred_nat^+"
-  le_def: "m \<le> (n::nat) == ~ (n < m)" ..
+  le_def:   "m \<le> (n::nat) == ~ (n < m)" ..
+
+lemmas [code nofunc] = less_def le_def
 
 text {* Induction *}
 
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Presburger.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -1069,11 +1069,12 @@
 lemma eq_number_of [code func]:
   "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
   unfolding number_of_is_id ..
+
 lemma eq_Pls_Pls:
-  "Numeral.Pls = Numeral.Pls" ..
+  "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by rule+
 
 lemma eq_Pls_Min:
-  "Numeral.Pls \<noteq> Numeral.Min"
+  "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
   unfolding Pls_def Min_def by auto
 
 lemma eq_Pls_Bit0:
@@ -1081,18 +1082,18 @@
   unfolding Pls_def Bit_def bit.cases by auto
 
 lemma eq_Pls_Bit1:
-  "Numeral.Pls \<noteq> Numeral.Bit k bit.B1"
+  "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
   unfolding Pls_def Bit_def bit.cases by arith
 
 lemma eq_Min_Pls:
-  "Numeral.Min \<noteq> Numeral.Pls"
+  "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
   unfolding Pls_def Min_def by auto
 
 lemma eq_Min_Min:
-  "Numeral.Min = Numeral.Min" ..
+  "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by rule+
 
 lemma eq_Min_Bit0:
-  "Numeral.Min \<noteq> Numeral.Bit k bit.B0"
+  "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
   unfolding Min_def Bit_def bit.cases by arith
 
 lemma eq_Min_Bit1:
@@ -1104,11 +1105,11 @@
   unfolding Pls_def Bit_def bit.cases by auto
 
 lemma eq_Bit1_Pls:
-  "Numeral.Bit k bit.B1 \<noteq>  Numeral.Pls"
+  "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
   unfolding Pls_def Bit_def bit.cases by arith
 
 lemma eq_Bit0_Min:
-  "Numeral.Bit k bit.B0 \<noteq> Numeral.Min"
+  "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
   unfolding Min_def Bit_def bit.cases by arith
 
 lemma eq_Bit1_Min:
@@ -1140,10 +1141,10 @@
   unfolding number_of_is_id ..
 
 lemma less_eq_Pls_Pls:
-  "Numeral.Pls \<le> Numeral.Pls" ..
+  "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
 
 lemma less_eq_Pls_Min:
-  "\<not> (Numeral.Pls \<le> Numeral.Min)"
+  "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
   unfolding Pls_def Min_def by auto
 
 lemma less_eq_Pls_Bit:
@@ -1151,11 +1152,11 @@
   unfolding Pls_def Bit_def by (cases v) auto
 
 lemma less_eq_Min_Pls:
-  "Numeral.Min \<le> Numeral.Pls"
+  "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
   unfolding Pls_def Min_def by auto
 
 lemma less_eq_Min_Min:
-  "Numeral.Min \<le> Numeral.Min" ..
+  "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
 
 lemma less_eq_Min_Bit0:
   "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
@@ -1198,10 +1199,10 @@
   unfolding number_of_is_id ..
 
 lemma less_Pls_Pls:
-  "\<not> (Numeral.Pls < Numeral.Pls)" by auto
+  "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by auto
 
 lemma less_Pls_Min:
-  "\<not> (Numeral.Pls < Numeral.Min)"
+  "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
   unfolding Pls_def Min_def by auto
 
 lemma less_Pls_Bit0:
@@ -1213,11 +1214,11 @@
   unfolding Pls_def Bit_def by auto
 
 lemma less_Min_Pls:
-  "Numeral.Min < Numeral.Pls"
+  "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
   unfolding Pls_def Min_def by auto
 
 lemma less_Min_Min:
-  "\<not> (Numeral.Min < Numeral.Min)" by auto
+  "Numeral.Min < Numeral.Min \<longleftrightarrow> False" by auto
 
 lemma less_Min_Bit:
   "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Product_Type.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -104,10 +104,10 @@
   Pair_def:     "Pair a b == Abs_Prod (Pair_Rep a b)"
   fst_def:      "fst p == THE a. EX b. p = Pair a b"
   snd_def:      "snd p == THE b. EX a. p = Pair a b"
-  split_def:    "split == (%c p. c (fst p) (snd p))"
-  curry_def:    "curry == (%c x y. c (Pair x y))"
-  prod_fun_def: "prod_fun f g == split (%x y. Pair (f x) (g y))"
-  Sigma_def:    "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
+  split_def [code func]:    "split == (%c p. c (fst p) (snd p))"
+  curry_def [code func]:    "curry == (%c x y. c (Pair x y))"
+  prod_fun_def [code func]: "prod_fun f g == split (%x y. Pair (f x) (g y))"
+  Sigma_def [code func]:    "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
 
 abbreviation
   Times :: "['a set, 'b set] => ('a * 'b) set"
@@ -599,17 +599,22 @@
   done
 
 
-constdefs
-  upd_fst :: "('a => 'c) => 'a * 'b => 'c * 'b"
- "upd_fst f == prod_fun f id"
+definition
+  upd_fst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
+where
+  "upd_fst f = prod_fun f id"
 
-  upd_snd :: "('b => 'c) => 'a * 'b => 'a * 'c"
- "upd_snd f == prod_fun id f"
+definition
+  upd_snd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c"
+where
+  "upd_snd f = prod_fun id f"
 
-lemma upd_fst_conv [simp]: "upd_fst f (x,y) = (f x,y)" 
+lemma upd_fst_conv [simp, code func]:
+  "upd_fst f (x, y) = (f x, y)" 
   by (simp add: upd_fst_def)
 
-lemma upd_snd_conv [simp]: "upd_snd f (x,y) = (x,f y)" 
+lemma upd_snd_conv [simp, code func]:
+  "upd_snd f (x, y) = (x, f y)" 
   by (simp add: upd_snd_def)
 
 text {*
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Record.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -17,11 +17,10 @@
 lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   by simp
 
-constdefs K_record:: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
-"K_record c x \<equiv> c"
-
-lemma K_record_apply [simp]: "K_record c x = c"
-  by (simp add: K_record_def)
+definition
+  K_record:: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
+where
+  K_record_apply [simp]: "K_record c x = c"
 
 lemma K_record_comp [simp]: "(K_record c \<circ> f) = K_record c"
   by (rule ext) (simp add: K_record_apply comp_def)
diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Set.thy	Fri Apr 20 11:21:42 2007 +0200
@@ -145,8 +145,10 @@
   subscripts in Proof General. *}
 
 instance set :: (type) ord
-  subset_def:   "A <= B         == \<forall>x\<in>A. x \<in> B"
-  psubset_def:  "A < B          == (A::'a set) <= B & ~ A=B" ..
+  subset_def:  "A \<le> B \<equiv> \<forall>x\<in>A. x \<in> B"
+  psubset_def: "A < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
+
+lemmas [code nofunc] = subset_def psubset_def
 
 abbreviation
   subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
@@ -344,6 +346,8 @@
   Compl_def:    "- A            == {x. ~x:A}"
   set_diff_def: "A - B          == {x. x:A & ~x:B}" ..
 
+lemmas [code nofunc] = Compl_def set_diff_def
+
 defs
   Un_def:       "A Un B         == {x. x:A | x:B}"
   Int_def:      "A Int B        == {x. x:A & x:B}"
@@ -2126,6 +2130,8 @@
   sup_set_eq: "sup A B \<equiv> A \<union> B"
   by intro_classes (auto simp add: inf_set_eq sup_set_eq)
 
+lemmas [code nofunc] = inf_set_eq sup_set_eq
+
 
 subsection {* Basic ML bindings *}
 
diff -r e2b06bfe471a -r 5cbe966d67a2 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/Pure/Isar/ROOT.ML	Fri Apr 20 11:21:42 2007 +0200
@@ -11,6 +11,7 @@
 use "auto_bind.ML";
 use "local_syntax.ML";
 use "proof_context.ML";
+use "../axclass.ML";
 use "local_defs.ML";
 
 (*outer syntax*)
@@ -41,13 +42,17 @@
 use "net_rules.ML";
 use "induct_attrib.ML";
 
+(*code generator base*)
+use "../Tools/codegen_consts.ML";
+use "../Tools/codegen_func.ML";
+use "../Tools/codegen_data.ML";
+
 (*derived theory and proof elements*)
 use "local_theory.ML";
 use "calculation.ML";
 use "obtain.ML";
 use "locale.ML";
 use "spec_parse.ML";
-use "../axclass.ML";
 use "../Tools/class_package.ML";
 use "theory_target.ML";
 use "specification.ML";
diff -r e2b06bfe471a -r 5cbe966d67a2 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 20 11:21:42 2007 +0200
@@ -89,7 +89,7 @@
     (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
         P.!!! (P.list1 P.xname)) []
         -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single))
-      >> (fn (x, y) => Toplevel.theory (snd o AxClass.define_class x [] y)));
+      >> (fn (x, y) => Toplevel.theory (snd o ClassPackage.axclass_cmd x y)));
 
 
 (* types *)
@@ -432,11 +432,6 @@
            >> (fn (arities, defs) => ClassPackage.instance_arity_cmd arities defs)
     ) >> (Toplevel.print oo Toplevel.theory_to_proof));
 
-val print_classesP =
-  OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
-      o Toplevel.keep (ClassPackage.print_classes o Toplevel.theory_of)));
-
 end;
 
 
@@ -710,6 +705,16 @@
 
 
 
+(** code generation **)
+
+val code_datatypeP =
+  OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl (
+    Scan.repeat1 P.term
+    >> (Toplevel.theory o CodegenData.add_datatype_consts_cmd)
+  );
+
+
+
 (** diagnostic commands (for interactive mode only) **)
 
 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
@@ -752,6 +757,11 @@
   OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales));
 
+val print_classesP =
+  OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag
+    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
+      o Toplevel.keep (ClassPackage.print_classes o Toplevel.theory_of)));
+
 val print_localeP =
   OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
     (opt_bang -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
@@ -860,6 +870,11 @@
   OuterSyntax.improper_command "typ" "read and print type" K.diag
     (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
 
+val print_codesetupP =
+  OuterSyntax.improper_command "print_codesetup" "print code generator setup of this theory" K.diag
+    (Scan.succeed
+      (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
+        (CodegenData.print_codesetup o Toplevel.theory_of)));
 
 
 (** system commands (for interactive mode only) **)
@@ -994,6 +1009,8 @@
   apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
   cannot_undoP, redoP, undos_proofP, undoP, killP, interpretationP,
   interpretP,
+  (*code generation*)
+  code_datatypeP,
   (*diagnostic commands*)
   pretty_setmarginP, helpP, print_classesP, print_commandsP, print_contextP,
   print_theoryP, print_syntaxP, print_abbrevsP, print_factsP,
@@ -1003,7 +1020,7 @@
   print_methodsP, print_antiquotationsP, thy_depsP, class_depsP, thm_depsP,
   find_theoremsP, print_bindsP, print_casesP, print_stmtsP,
   print_thmsP, print_prfsP, print_full_prfsP, print_propP,
-  print_termP, print_typeP,
+  print_termP, print_typeP, print_codesetupP,
   (*system commands*)
   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,
diff -r e2b06bfe471a -r 5cbe966d67a2 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/Pure/Isar/specification.ML	Fri Apr 20 11:21:42 2007 +0200
@@ -130,7 +130,8 @@
 (*    |> LocalTheory.def ((x, mx), ((name ^ "_raw", []), rhs));  FIXME *)
       |> LocalTheory.def Thm.definitionK ((x, mx), ((name, []), rhs));
     val ((b, [th']), lthy3) = lthy2
-      |> LocalTheory.note Thm.definitionK ((name, atts), [prove lthy2 th]);
+      |> LocalTheory.note Thm.definitionK
+          ((name, CodegenData.add_func_attr false :: atts), [prove lthy2 th]);
 
     val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
     val _ = print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
diff -r e2b06bfe471a -r 5cbe966d67a2 src/Pure/Tools/ROOT.ML
--- a/src/Pure/Tools/ROOT.ML	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/Pure/Tools/ROOT.ML	Fri Apr 20 11:21:42 2007 +0200
@@ -15,9 +15,6 @@
 use "../codegen.ML";
 
 (*code generator, 2nd generation*)
-use "codegen_consts.ML";
-use "codegen_func.ML";
-use "codegen_data.ML";
 use "codegen_names.ML";
 use "codegen_funcgr.ML";
 use "codegen_thingol.ML";
diff -r e2b06bfe471a -r 5cbe966d67a2 src/Pure/Tools/codegen_data.ML
--- a/src/Pure/Tools/codegen_data.ML	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/Pure/Tools/codegen_data.ML	Fri Apr 20 11:21:42 2007 +0200
@@ -14,6 +14,7 @@
   val add_func: bool -> thm -> theory -> theory
   val del_func: thm -> theory -> theory
   val add_funcl: CodegenConsts.const * thm list Susp.T -> theory -> theory
+  val add_func_attr: bool -> Attrib.src
   val add_inline: thm -> theory -> theory
   val del_inline: thm -> theory -> theory
   val add_inline_proc: string * (theory -> cterm list -> thm list) -> theory -> theory
@@ -23,6 +24,7 @@
   val add_datatype: string * ((string * sort) list * (string * typ list) list)
     -> theory -> theory
   val add_datatype_consts: CodegenConsts.const list -> theory -> theory
+  val add_datatype_consts_cmd: string list -> theory -> theory
 
   val coregular_algebra: theory -> Sorts.algebra
   val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
@@ -33,6 +35,8 @@
 
   val preprocess_cterm: cterm -> thm
 
+  val print_codesetup: theory -> unit
+
   val trace: bool ref
 end;
 
@@ -91,7 +95,7 @@
   then (false, xs)
   else (true, AList.merge eq_key eq xys);
 
-val merge_thms = merge' Thm.eq_thm;
+val merge_thms = merge' Thm.eq_thm_prop;
 
 fun merge_lthms (r1, r2) =
   if Susp.same (r1, r2)
@@ -122,7 +126,7 @@
     fun drop thm' = not (matches args (args_of thm'))
       orelse (warning ("Dropping redundant defining equation\n" ^ string_of_thm thm'); false);
     val (keeps, drops) = List.partition drop sels;
-  in (thm :: keeps, dels |> fold (insert Thm.eq_thm) drops |> remove Thm.eq_thm thm) end;
+  in (thm :: keeps, dels |> fold (insert Thm.eq_thm_prop) drops |> remove Thm.eq_thm_prop thm) end;
 
 fun add_thm thm (sels, dels) =
   apfst Susp.value (add_drop_redundant thm (Susp.force sels, dels));
@@ -135,7 +139,7 @@
       fold add_thm (Susp.force lthms) (sels, dels);
 
 fun del_thm thm (sels, dels) =
-  (Susp.value (remove Thm.eq_thm thm (Susp.force sels)), thm :: dels);
+  (Susp.value (remove Thm.eq_thm_prop thm (Susp.force sels)), thm :: dels);
 
 fun pretty_sdthms ctxt (sels, _) = pretty_lthms ctxt sels;
 
@@ -144,8 +148,8 @@
     val (dels_t, dels) = merge_thms (dels1, dels2);
   in if dels_t
     then let
-      val (_, sels) = merge_thms (Susp.force sels1, subtract Thm.eq_thm dels1 (Susp.force sels2))
-      val (_, dels) = merge_thms (dels1, subtract Thm.eq_thm (Susp.force sels1) dels2)
+      val (_, sels) = merge_thms (Susp.force sels1, subtract Thm.eq_thm_prop dels1 (Susp.force sels2))
+      val (_, dels) = merge_thms (dels1, subtract Thm.eq_thm_prop (Susp.force sels1) dels2)
     in (true, ((lazy_thms o K) sels, dels)) end
     else let
       val (sels_t, sels) = merge_lthms (sels1, sels2)
@@ -377,6 +381,8 @@
     end;
 end);
 
+val print_codesetup = CodeData.print;
+
 fun init k = CodeData.map
   (fn (exec, data) => (exec, ref (Datatab.update (k, invoke_empty k) (! data))));
 
@@ -402,16 +408,16 @@
 
 fun common_typ_funcs [] = []
   | common_typ_funcs [thm] = [thm]
-  | common_typ_funcs thms =
+  | common_typ_funcs (thms as thm :: _) =
       let
-        val thy = Thm.theory_of_thm (hd thms)
+        val thy = Thm.theory_of_thm thm;
         fun incr_thm thm max =
           let
             val thm' = incr_indexes max thm;
             val max' = Thm.maxidx_of thm' + 1;
           in (thm', max') end;
         val (thms', maxidx) = fold_map incr_thm thms 0;
-        val (ty1::tys) = map CodegenFunc.typ_func thms';
+        val ty1 :: tys = map (snd o CodegenFunc.head_func) thms';
         fun unify ty env = Sign.typ_unify thy (ty1, ty) env
           handle Type.TUNIFY =>
             error ("Type unificaton failed, while unifying defining equations\n"
@@ -423,12 +429,12 @@
           cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
       in map (Thm.instantiate (instT, [])) thms' end;
 
-fun certify_const thy c c_thms =
+fun certify_const thy const thms =
   let
-    fun cert (c', thm) = if CodegenConsts.eq_const (c, c')
+    fun cert thm = if CodegenConsts.eq_const (const, fst (CodegenFunc.head_func thm))
       then thm else error ("Wrong head of defining equation,\nexpected constant "
-        ^ CodegenConsts.string_of_const thy c ^ "\n" ^ string_of_thm thm)
-  in map cert c_thms end;
+        ^ CodegenConsts.string_of_const thy const ^ "\n" ^ string_of_thm thm)
+  in map cert thms end;
 
 
 
@@ -459,7 +465,7 @@
       |> maps these
       |> map (Thm.transfer thy);
     val sorts = map (map (snd o dest_TVar) o snd o dest_Type o the_single
-      o Sign.const_typargs thy o fst o CodegenFunc.dest_func) funcs;
+      o Sign.const_typargs thy o (fn ((c, _), ty) => (c, ty)) o CodegenFunc.head_func) funcs;
   in sorts end;
 
 fun weakest_constraints thy (class, tyco) =
@@ -512,51 +518,49 @@
 val classop_weakest_typ = gen_classop_typ weakest_constraints;
 val classop_strongest_typ = gen_classop_typ strongest_constraints;
 
-fun gen_mk_func_typ strict thm =
+fun assert_func_typ thm =
   let
     val thy = Thm.theory_of_thm thm;
-    val raw_funcs = CodegenFunc.mk_func strict thm;
-    val error_warning = if strict then error else warning #> K NONE;
     fun check_typ_classop class (const as (c, SOME tyco), thm) =
           let
-            val ((_, ty), _) = CodegenFunc.dest_func thm;
+            val (_, ty) = CodegenFunc.head_func thm;
             val ty_decl = classop_weakest_typ thy class (c, tyco);
             val ty_strongest = classop_strongest_typ thy class (c, tyco);
             fun constrain thm = 
               let
                 val max = Thm.maxidx_of thm + 1;
                 val ty_decl' = Logic.incr_tvar max ty_decl;
-                val ((_, ty'), _) = CodegenFunc.dest_func thm;
+                val (_, ty') = CodegenFunc.head_func thm;
                 val (env, _) = Sign.typ_unify thy (ty_decl', ty') (Vartab.empty, max);
                 val instT = Vartab.fold (fn (x_i, (sort, ty)) =>
                   cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
               in Thm.instantiate (instT, []) thm end;
           in if Sign.typ_instance thy (ty_strongest, ty)
             then if Sign.typ_instance thy (ty, ty_decl)
-            then SOME (const, thm)
+            then thm
             else (warning ("Constraining type\n" ^ CodegenConsts.string_of_typ thy ty
               ^ "\nof defining equation\n"
               ^ string_of_thm thm
               ^ "\nto permitted most general type\n"
               ^ CodegenConsts.string_of_typ thy ty_decl);
-              SOME (const, constrain thm))
-            else error_warning ("Type\n" ^ CodegenConsts.string_of_typ thy ty
+              constrain thm)
+            else CodegenFunc.bad_thm ("Type\n" ^ CodegenConsts.string_of_typ thy ty
               ^ "\nof defining equation\n"
               ^ string_of_thm thm
               ^ "\nis incompatible with permitted least general type\n"
               ^ CodegenConsts.string_of_typ thy ty_strongest)
           end
       | check_typ_classop class ((c, NONE), thm) =
-          error_warning ("Illegal type for class operation " ^ quote c
+          CodegenFunc.bad_thm ("Illegal type for class operation " ^ quote c
            ^ "\nin defining equation\n"
            ^ string_of_thm thm);
     fun check_typ_fun (const as (c, _), thm) =
       let
-        val ((_, ty), _) = CodegenFunc.dest_func thm;
+        val (_, ty) = CodegenFunc.head_func thm;
         val ty_decl = Sign.the_const_type thy c;
       in if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
-        then SOME (const, thm)
-        else error_warning ("Type\n" ^ CodegenConsts.string_of_typ thy ty
+        then thm
+        else CodegenFunc.bad_thm ("Type\n" ^ CodegenConsts.string_of_typ thy ty
            ^ "\nof defining equation\n"
            ^ string_of_thm thm
            ^ "\nis incompatible declared function type\n"
@@ -566,23 +570,34 @@
       case AxClass.class_of_param thy c
        of SOME class => check_typ_classop class (const, thm)
         | NONE => check_typ_fun (const, thm);
-    val funcs = map_filter check_typ raw_funcs;
-  in funcs end;
+  in check_typ (fst (CodegenFunc.head_func thm), thm) end;
+
+val mk_func = CodegenFunc.error_thm
+  (assert_func_typ o CodegenFunc.mk_func);
+val mk_func_liberal = CodegenFunc.warning_thm
+  (assert_func_typ o CodegenFunc.mk_func);
 
 end;
 
-
 (** interfaces **)
 
-fun add_func strict thm thy =
-  let
-    val funcs = gen_mk_func_typ strict thm;
-    val cs = map fst funcs;
-  in
-    map_exec_purge (SOME cs) (map_funcs 
-     (fold (fn (c, thm) => Consttab.map_default
-       (c, (Susp.value [], [])) (add_thm thm)) funcs)) thy
-  end;
+fun add_func true thm thy =
+      let
+        val func = mk_func thm;
+        val (const, _) = CodegenFunc.head_func func;
+      in map_exec_purge (SOME [const]) (map_funcs
+        (Consttab.map_default
+          (const, (Susp.value [], [])) (add_thm func))) thy
+      end
+  | add_func false thm thy =
+      case mk_func_liberal thm
+       of SOME func => let
+              val (const, _) = CodegenFunc.head_func func
+            in map_exec_purge (SOME [const]) (map_funcs
+              (Consttab.map_default
+                (const, (Susp.value [], [])) (add_thm func))) thy
+            end
+        | NONE => thy;
 
 fun delete_force msg key xs =
   if AList.defined (op =) xs key then AList.delete (op =) key xs
@@ -590,23 +605,26 @@
 
 fun del_func thm thy =
   let
-    val funcs = gen_mk_func_typ false thm;
-    val cs = map fst funcs;
-  in
-    map_exec_purge (SOME cs) (map_funcs
-     (fold (fn (c, thm) => Consttab.map_entry c
-       (del_thm thm)) funcs)) thy
+    val func = mk_func thm;
+    val (const, _) = CodegenFunc.head_func func;
+  in map_exec_purge (SOME [const]) (map_funcs
+    (Consttab.map_entry
+      const (del_thm func))) thy
   end;
 
 fun add_funcl (const, lthms) thy =
   let
-    val lthms' = certificate thy (fn thy => certify_const thy const
-      o maps (CodegenFunc.mk_func true)) lthms;
+    val lthms' = certificate thy (fn thy => certify_const thy const) lthms;
+      (*FIXME must check compatibility with sort algebra;
+        alas, naive checking results in non-termination!*)
   in
     map_exec_purge (SOME [const]) (map_funcs (Consttab.map_default (const, (Susp.value [], []))
       (add_lthms lthms'))) thy
   end;
 
+fun add_func_attr strict = Attrib.internal (fn _ => Thm.declaration_attribute
+  (fn thm => Context.mapping (add_func strict thm) I));
+
 local
 
 fun del_datatype tyco thy =
@@ -637,12 +655,12 @@
 
 fun add_inline thm thy =
   (map_exec_purge NONE o map_preproc o apfst o apfst)
-    (fold (insert Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy;
+    (insert Thm.eq_thm_prop (CodegenFunc.mk_rew thm)) thy;
         (*fully applied in order to get right context for mk_rew!*)
 
 fun del_inline thm thy =
   (map_exec_purge NONE o map_preproc o apfst o apfst)
-    (fold (remove Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy;
+    (remove Thm.eq_thm_prop (CodegenFunc.mk_rew thm)) thy;
         (*fully applied in order to get right context for mk_rew!*)
 
 fun add_inline_proc (name, f) =
@@ -680,12 +698,9 @@
 fun apply_preproc thy f [] = []
   | apply_preproc thy f (thms as (thm :: _)) =
       let
+        val (const, _) = CodegenFunc.head_func thm;
         val thms' = f thy thms;
-        val thms'' as ((const, _) :: _) = map CodegenFunc.mk_head thms'
-      in (certify_const thy const o map CodegenFunc.mk_head) thms' end;
-
-fun cmp_thms thy =
-  make_ord (fn (thm1, thm2) => not (Sign.typ_instance thy (CodegenFunc.typ_func thm1, CodegenFunc.typ_func thm2)));
+      in certify_const thy const thms' end;
 
 fun rhs_conv conv thm =
   let
@@ -700,7 +715,6 @@
   |> map (CodegenFunc.rewrite_func ((#inlines o the_preproc o get_exec) thy))
   |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_preproc o get_exec) thy)
 (*FIXME - must check: rewrite rule, defining equation, proper constant |> map (snd o check_func false thy) *)
-  |> sort (cmp_thms thy)
   |> common_typ_funcs;
 
 fun preprocess_cterm ct =
@@ -757,38 +771,14 @@
   |> these
   |> map (Thm.transfer thy);
 
-fun find_def thy (const as (c, _)) =
-  let
-    val specs = Defs.specifications_of (Theory.defs_of thy) c;
-    val ty = case try (default_typ_proto thy) const
-     of NONE => NONE
-      | SOME ty => ty;
-    val tys = Sign.const_typargs thy (c, ty |> the_default (Sign.the_const_type thy c));
-    fun get_def (_, { is_def, name, lhs, rhs, thyname }) =
-      if is_def andalso forall (Sign.typ_instance thy) (tys ~~ lhs) then
-        try (Thm.get_axiom_i thy) name
-      else NONE
-  in get_first get_def specs end;
-
 in
 
 fun these_funcs thy const =
   let
-    fun get_prim_def_funcs (const as (c, tys)) =
-      case find_def thy const
-       of SOME thm =>
-            thm
-            |> Thm.transfer thy
-            |> gen_mk_func_typ false
-            |> map (CodegenFunc.expand_eta ~1 o snd)
-        | NONE => []
     fun drop_refl thy = filter_out (is_equal o Term.fast_term_ord o Logic.dest_equals
       o ObjectLogic.drop_judgment thy o Thm.plain_prop_of);
-    val funcs = case get_funcs thy const
-     of [] => get_prim_def_funcs const
-    | funcs => funcs
   in
-    funcs
+    get_funcs thy const
     |> preprocess thy
     |> drop_refl thy
   end;
@@ -796,61 +786,14 @@
 fun default_typ thy (const as (c, _)) = case default_typ_proto thy const
  of SOME ty => ty
   | NONE => (case get_funcs thy const
-     of thm :: _ => CodegenFunc.typ_func thm
+     of thm :: _ => snd (CodegenFunc.head_func thm)
       | [] => Sign.the_const_type thy c);
 
 end; (*local*)
 
-
-(** code attributes **)
-
-local
-  fun add_simple_attribute (name, f) =
-    (Codegen.add_attribute name o (Scan.succeed o Thm.declaration_attribute))
-      (fn th => Context.mapping (f th) I);
-in
-  val _ = map (Context.add_setup o add_simple_attribute) [
-    ("func", add_func true),
-    ("nofunc", del_func),
-    ("unfold", (fn thm => Codegen.add_unfold thm #> add_inline thm)),
-    ("inline", add_inline),
-    ("noinline", del_inline)
-  ]
-end; (*local*)
-
-
-(** Isar setup **)
-
-local
-
-structure P = OuterParse
-and K = OuterKeyword
-
-val print_codesetupK = "print_codesetup";
-val code_datatypeK = "code_datatype";
-
-in
-
-val print_codesetupP =
-  OuterSyntax.improper_command print_codesetupK "print code generator setup of this theory" K.diag
-    (Scan.succeed
-      (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep (CodeData.print o Toplevel.theory_of)));
-
-val code_datatypeP =
-  OuterSyntax.command code_datatypeK "define set of code datatype constructors" K.thy_decl (
-    Scan.repeat1 P.term
-    >> (Toplevel.theory o add_datatype_consts_cmd)
-  );
-
-
-val _ = OuterSyntax.add_parsers [print_codesetupP, code_datatypeP];
-
-end; (*local*)
-
 end; (*struct*)
 
 
-
 (** type-safe interfaces for data depedent on executable content **)
 
 signature CODE_DATA_ARGS =