tuned

--- a/src/HOL/Extraction/Pigeonhole.thy	Fri Apr 20 11:21:34 2007 +0200
+++ b/src/HOL/Extraction/Pigeonhole.thy	Fri Apr 20 11:21:35 2007 +0200
@@ -5,7 +5,9 @@
 
 header {* The pigeonhole principle *}
 
-theory Pigeonhole imports EfficientNat begin
+theory Pigeonhole
+imports EfficientNat
+begin
 
 text {*
 We formalize two proofs of the pigeonhole principle, which lead

--- a/src/HOL/Lattices.thy	Fri Apr 20 11:21:34 2007 +0200
+++ b/src/HOL/Lattices.thy	Fri Apr 20 11:21:35 2007 +0200
@@ -13,18 +13,20 @@
 
 text{*
   This theory of lattices only defines binary sup and inf
-  operations. The extension to (finite) sets is done in theories @{text FixedPoint}
-  and @{text Finite_Set}.
+  operations. The extension to (finite) sets is done in theories
+  @{text FixedPoint} and @{text Finite_Set}.
 *}
 
 class lower_semilattice = order +
   fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
-  assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
+  assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
+  and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
   and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
 
 class upper_semilattice = order +
   fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
-  assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
+  assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
+  and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
   and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
 
 class lattice = lower_semilattice + upper_semilattice
@@ -251,28 +253,28 @@
 
 subsection {* Uniqueness of inf and sup *}
 
-lemma inf_unique:
+lemma (in lower_semilattice) inf_unique:
   fixes f (infixl "\<triangle>" 70)
-  assumes le1: "\<And>x y. x \<triangle> y \<le> x" and le2: "\<And>x y. x \<triangle> y \<le> y"
-  and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
-  shows "inf x y = f x y"
+  assumes le1: "\<And>x y. x \<triangle> y \<^loc>\<le> x" and le2: "\<And>x y. x \<triangle> y \<^loc>\<le> y"
+  and greatest: "\<And>x y z. x \<^loc>\<le> y \<Longrightarrow> x \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> y \<triangle> z"
+  shows "x \<sqinter> y = x \<triangle> y"
 proof (rule antisym)
-  show "x \<triangle> y \<le> inf x y" by (rule le_infI) (rule le1 le2)
+  show "x \<triangle> y \<^loc>\<le> x \<sqinter> y" by (rule le_infI) (rule le1 le2)
 next
-  have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" by (blast intro: greatest)
-  show "inf x y \<le> x \<triangle> y" by (rule leI) simp_all
+  have leI: "\<And>x y z. x \<^loc>\<le> y \<Longrightarrow> x \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> y \<triangle> z" by (blast intro: greatest)
+  show "x \<sqinter> y \<^loc>\<le> x \<triangle> y" by (rule leI) simp_all
 qed
 
-lemma sup_unique:
+lemma (in upper_semilattice) sup_unique:
   fixes f (infixl "\<nabla>" 70)
-  assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y" and ge2: "\<And>x y. y \<le> x \<nabla> y"
-  and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x"
-  shows "sup x y = f x y"
+  assumes ge1 [simp]: "\<And>x y. x \<^loc>\<le> x \<nabla> y" and ge2: "\<And>x y. y \<^loc>\<le> x \<nabla> y"
+  and least: "\<And>x y z. y \<^loc>\<le> x \<Longrightarrow> z \<^loc>\<le> x \<Longrightarrow> y \<nabla> z \<^loc>\<le> x"
+  shows "x \<squnion> y = x \<nabla> y"
 proof (rule antisym)
-  show "sup x y \<le> x \<nabla> y" by (rule le_supI) (rule ge1 ge2)
+  show "x \<squnion> y \<^loc>\<le> x \<nabla> y" by (rule le_supI) (rule ge1 ge2)
 next
-  have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z" by (blast intro: least)
-  show "x \<nabla> y \<le> sup x y" by (rule leI) simp_all
+  have leI: "\<And>x y z. x \<^loc>\<le> z \<Longrightarrow> y \<^loc>\<le> z \<Longrightarrow> x \<nabla> y \<^loc>\<le> z" by (blast intro: least)
+  show "x \<nabla> y \<^loc>\<le> x \<squnion> y" by (rule leI) simp_all
 qed
   
 

--- a/src/HOL/Relation_Power.thy	Fri Apr 20 11:21:34 2007 +0200
+++ b/src/HOL/Relation_Power.thy	Fri Apr 20 11:21:35 2007 +0200
@@ -40,7 +40,8 @@
 *}
 
 definition
-  funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+  funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
+where
   funpow_def: "funpow n f = f ^ n"
 
 lemmas [code inline] = funpow_def [symmetric]

--- a/src/HOL/ex/Records.thy	Fri Apr 20 11:21:34 2007 +0200
+++ b/src/HOL/ex/Records.thy	Fri Apr 20 11:21:35 2007 +0200
@@ -35,17 +35,21 @@
   'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr>  = 'a point_ext_type"}
 *}
 
-consts foo1 :: point
 consts foo2 :: "(| xpos :: nat, ypos :: nat |)"
-consts foo3 :: "'a => 'a point_scheme"
 consts foo4 :: "'a => (| xpos :: nat, ypos :: nat, ... :: 'a |)"
 
 
 subsubsection {* Introducing concrete records and record schemes *}
 
-defs
-  foo1_def: "foo1 == (| xpos = 1, ypos = 0 |)"
-  foo3_def: "foo3 ext == (| xpos = 1, ypos = 0, ... = ext |)"
+definition
+  foo1 :: point
+where
+  foo1_def: "foo1 = (| xpos = 1, ypos = 0 |)"
+
+definition
+  foo3 :: "'a => 'a point_scheme"
+where
+  foo3_def: "foo3 ext = (| xpos = 1, ypos = 0, ... = ext |)"
 
 
 subsubsection {* Record selection and record update *}

--- a/src/Pure/Tools/class_package.ML	Fri Apr 20 11:21:34 2007 +0200
+++ b/src/Pure/Tools/class_package.ML	Fri Apr 20 11:21:35 2007 +0200
@@ -9,6 +9,8 @@
 sig
   val fork_mixfix: bool -> string option -> mixfix -> mixfix * mixfix
 
+  val axclass_cmd: bstring * xstring list
+    -> ((bstring * Attrib.src list) * string list) list -> theory -> class * theory
   val class: bstring -> class list -> Element.context_i Locale.element list
     -> string list -> theory -> string * Proof.context
   val class_cmd: bstring -> string list -> Element.context Locale.element list
@@ -45,10 +47,21 @@
 fun fork_mixfix is_loc some_class mx =
   let
     val mx' = Syntax.unlocalize_mixfix mx;
-    val mx_global = if is_some some_class orelse (is_loc andalso mx = mx') then NoSyn else mx';
+    val mx_global = if is_some some_class orelse (is_loc andalso mx = mx')
+      then NoSyn else mx';
     val mx_local = if is_loc then mx else NoSyn;
   in (mx_global, mx_local) end;
 
+fun axclass_cmd (class, raw_superclasses) raw_specs thy =
+  let
+    val ctxt = ProofContext.init thy;
+    val superclasses = map (Sign.read_class thy) raw_superclasses;
+    val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst) raw_specs;
+    val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd) raw_specs)
+      |> snd
+      |> (map o map) fst;
+  in AxClass.define_class (class, superclasses) [] (name_atts ~~ axiomss) thy end;
+
 
 (** AxClasses with implicit parameter handling **)
 
@@ -95,7 +108,7 @@
     thy
     |> fold_map add_const consts
     |-> (fn cs => mk_axioms cs
-    #-> (fn axioms_prop => AxClass.define_class_i (name, superclasses) (map fst cs @ other_consts) axioms_prop
+    #-> (fn axioms_prop => AxClass.define_class (name, superclasses) (map fst cs @ other_consts) axioms_prop
     #-> (fn class => `(fn thy => AxClass.get_definition thy class)
     #-> (fn {intro, axioms, ...} => fold (add_constraint class) cs
     #> pair (class, ((intro, (map Thm.prop_of axioms, axioms)), cs))))))
@@ -177,14 +190,15 @@
       thy
       |> PureThy.add_defs_i true (map ((apsnd o map) (Attrib.attribute thy) o snd) defs)
       |-> (fn thms => pair (map fst defs ~~ thms));
-    fun after_qed cs thy =
+    fun after_qed cs defs thy =
       thy
-      |> fold Sign.add_const_constraint_i (map (apsnd SOME) cs);
+      |> fold Sign.add_const_constraint_i (map (apsnd SOME) cs)
+      |> fold (CodegenData.add_func false o snd) defs;
   in
     theory
     |> fold_map get_remove_contraint (map fst cs |> distinct (op =))
     ||>> add_defs defs
-    |-> (fn (cs, _) => do_proof (after_qed cs) arities)
+    |-> (fn (cs, defs) => do_proof (after_qed cs defs) arities)
   end;
 
 fun instance_arity_e' do_proof = gen_instance_arity Sign.read_arity read_def_cmd do_proof;
@@ -343,20 +357,6 @@
 
 (* tactics and methods *)
 
-(*FIXME adjust these when minimal intro rules are at hand*)
-fun intro_classes_tac' facts st =
-  let
-    val thy = Thm.theory_of_thm st;
-    val ctxt = ProofContext.init thy;
-    val intro_classes_tac = ALLGOALS
-      (Method.insert_tac facts THEN' REPEAT_ALL_NEW (resolve_tac (AxClass.class_intros thy)))
-        THEN Tactic.distinct_subgoals_tac;
-    val intro_locales_tac = SOMEGOAL (SELECT_GOAL (Locale.intro_locales_tac true ctxt facts))
-      THEN Tactic.distinct_subgoals_tac;
-  in
-    (intro_classes_tac THEN REPEAT (intro_locales_tac ORELSE intro_locales_tac)) st
-  end;
-
 fun intro_classes_tac facts st =
   let
     val thy = Thm.theory_of_thm st;
@@ -381,9 +381,7 @@
     default_intro_classes_tac facts;
 
 val _ = Context.add_setup (Method.add_methods
- [("intro_classes2", Method.no_args (Method.METHOD intro_classes_tac'),
-    "back-chain introduction rules of classes"),
-  ("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
+ [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
     "back-chain introduction rules of classes"),
   ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
     "apply some intro/elim rule")]);
@@ -481,6 +479,14 @@
 
 local
 
+fun read_param thy raw_t =
+  let
+    val t = Sign.read_term thy raw_t
+  in case try dest_Const t
+   of SOME (c, _) => c
+    | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
+  end;
+
 fun gen_class add_locale prep_class prep_param bname
     raw_supclasses raw_elems raw_other_consts thy =
   let
@@ -573,7 +579,7 @@
 
 in
 
-val class_cmd = gen_class Locale.add_locale Sign.intern_class AxClass.read_param;
+val class_cmd = gen_class Locale.add_locale Sign.intern_class read_param;
 val class = gen_class Locale.add_locale_i Sign.certify_class (K I);
 
 end; (*local*)
@@ -643,7 +649,7 @@
       thy
       |> PureThy.add_defs_i false [((name, prop), map (Attrib.attribute thy) atts)]
       |>> the_single;
-    val _ = warning "------ DEF ------";
+    (*val _ = warning "------ DEF ------";
     val _ = warning c;
     val _ = warning name;
     val _ = (warning o Sign.string_of_term thy) rhs';
@@ -658,14 +664,14 @@
     val _ = map print_witness witness;
     val _ = (warning o string_of_thm) eq';
     val eq'' = Element.satisfy_thm witness eq';
-    val _ = (warning o string_of_thm) eq'';
+    val _ = (warning o string_of_thm) eq'';*)
   in
     thy
-    |> Sign.add_path prfx
+    (* |> Sign.add_path prfx
     |> add_const (c, ty, syn')
     |-> (fn c => add_def ((name, atts), Logic.mk_equals (Const c, rhs')))
     |-> (fn global_def_thm => tap (fn _ => (warning o string_of_thm) global_def_thm))
-    |> Sign.restore_naming thy
+    |> Sign.restore_naming thy *)
   end;
 
 end;

--- a/src/Pure/Tools/codegen_consts.ML	Fri Apr 20 11:21:34 2007 +0200
+++ b/src/Pure/Tools/codegen_consts.ML	Fri Apr 20 11:21:35 2007 +0200
@@ -16,6 +16,8 @@
   val string_of_typ: theory -> typ -> string
   val string_of_const: theory -> const -> string
   val read_const: theory -> string -> const
+  val read_const_exprs: theory -> (const list -> const list)
+    -> string list -> const list
 
   val co_of_const: theory -> const
     -> string * ((string * sort) list * (string * typ list))
@@ -68,7 +70,7 @@
       ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco);
 
 
-(* reading constants as terms *)
+(* reading constants as terms and wildcards pattern *)
 
 fun read_const thy raw_t =
   let
@@ -78,6 +80,47 @@
     | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
   end;
 
+local
+
+fun consts_of thy some_thyname =
+  let
+    val this_thy = Option.map theory some_thyname |> the_default thy;
+    val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
+      ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy) [];
+    fun classop c = case AxClass.class_of_param thy c
+     of NONE => [(c, NONE)]
+      | SOME class => Symtab.fold
+          (fn (tyco, classes) => if AList.defined (op =) classes class
+            then cons (c, SOME tyco) else I)
+          ((#arities o Sorts.rep_algebra o Sign.classes_of) this_thy)
+          [(c, NONE)];
+    val consts = maps classop cs;
+    fun test_instance thy (class, tyco) =
+      can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
+    fun belongs_here thyname (c, NONE) =
+          not (exists (fn thy' => Sign.declared_const thy' c) (Theory.parents_of this_thy))
+      | belongs_here thyname (c, SOME tyco) =
+          let
+            val SOME class = AxClass.class_of_param thy c
+          in not (exists (fn thy' => test_instance thy' (class, tyco))
+            (Theory.parents_of this_thy))
+          end;
+  in case some_thyname
+   of NONE => consts
+    | SOME thyname => filter (belongs_here thyname) consts
+  end;
+
+fun read_const_expr thy "*" = ([], consts_of thy NONE)
+  | read_const_expr thy s = if String.isSuffix ".*" s
+      then ([], consts_of thy (SOME (unsuffix ".*" s)))
+      else ([read_const thy s], []);
+
+in
+
+fun read_const_exprs thy select =
+  (op @) o apsnd select o pairself flat o split_list o map (read_const_expr thy);
+
+end; (*local*)
 
 (* conversion between constants, constant expressions and datatype constructors *)
 

--- a/src/Pure/Tools/codegen_func.ML	Fri Apr 20 11:21:34 2007 +0200
+++ b/src/Pure/Tools/codegen_func.ML	Fri Apr 20 11:21:35 2007 +0200
@@ -8,12 +8,12 @@
 signature CODEGEN_FUNC =
 sig
   val assert_rew: thm -> thm
-  val mk_rew: thm -> thm list
-  val assert_func: bool -> thm -> thm option
-  val mk_func: bool -> thm -> (CodegenConsts.const * thm) list
-  val mk_head: thm -> CodegenConsts.const * thm
-  val dest_func: thm -> (string * typ) * term list
-  val typ_func: thm -> typ
+  val mk_rew: thm -> thm
+  val mk_func: thm -> thm
+  val head_func: thm -> CodegenConsts.const * typ
+  val bad_thm: string -> 'a
+  val error_thm: (thm -> thm) -> thm -> thm
+  val warning_thm: (thm -> thm) -> thm -> thm option
 
   val inst_thm: sort Vartab.table -> thm -> thm
   val expand_eta: int -> thm -> thm
@@ -25,10 +25,14 @@
 structure CodegenFunc : CODEGEN_FUNC =
 struct
 
-fun lift_thm_thy f thm = f (Thm.theory_of_thm thm) thm;
+
+(* auxiliary *)
 
-fun bad_thm msg thm =
-  error (msg ^ ": " ^ string_of_thm thm);
+exception BAD_THM of string;
+fun bad_thm msg = raise BAD_THM msg;
+fun error_thm f thm = f thm handle BAD_THM msg => error msg;
+fun warning_thm f thm = SOME (f thm) handle BAD_THM msg
+  => (warning msg; NONE);
 
 
 (* making rewrite theorems *)
@@ -36,85 +40,82 @@
 fun assert_rew thm =
   let
     val thy = Thm.theory_of_thm thm;
-    val (lhs, rhs) = (Logic.dest_equals o Thm.prop_of) thm;
+    val (lhs, rhs) = (Logic.dest_equals o Thm.prop_of) thm
+      handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
     fun vars_of t = fold_aterms
      (fn Var (v, _) => insert (op =) v
-       | Free _ => bad_thm "Illegal free variable in rewrite theorem" thm
+       | Free _ => bad_thm ("Illegal free variable in rewrite theorem\n"
+           ^ Display.string_of_thm thm)
        | _ => I) t [];
     fun tvars_of t = fold_term_types
      (fn _ => fold_atyps (fn TVar (v, _) => insert (op =) v
-                          | TFree _ => bad_thm "Illegal free type variable in rewrite theorem" thm)) t [];
+                          | TFree _ => bad_thm 
+      ("Illegal free type variable in rewrite theorem\n" ^ Display.string_of_thm thm))) t [];
     val lhs_vs = vars_of lhs;
     val rhs_vs = vars_of rhs;
     val lhs_tvs = tvars_of lhs;
     val rhs_tvs = tvars_of lhs;
     val _ = if null (subtract (op =) lhs_vs rhs_vs)
       then ()
-      else bad_thm "Free variables on right hand side of rewrite theorems" thm
+      else bad_thm ("Free variables on right hand side of rewrite theorem\n"
+        ^ Display.string_of_thm thm);
     val _ = if null (subtract (op =) lhs_tvs rhs_tvs)
       then ()
-      else bad_thm "Free type variables on right hand side of rewrite theorems" thm
+      else bad_thm ("Free type variables on right hand side of rewrite theorem\n"
+        ^ Display.string_of_thm thm)
   in thm end;
 
 fun mk_rew thm =
   let
     val thy = Thm.theory_of_thm thm;
-    val thms = (#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy thm;
+    val ctxt = ProofContext.init thy;
   in
-    map assert_rew thms
+    thm
+    |> LocalDefs.meta_rewrite_rule ctxt
+    |> assert_rew
   end;
 
 
 (* making defining equations *)
 
-val typ_func = lift_thm_thy (fn thy => snd o dest_Const o fst o strip_comb
-  o fst o Logic.dest_equals o ObjectLogic.drop_judgment thy o Thm.plain_prop_of);
-
-val dest_func = lift_thm_thy (fn thy => apfst dest_Const o strip_comb
-  o fst o Logic.dest_equals o ObjectLogic.drop_judgment thy o Thm.plain_prop_of
-  o Drule.fconv_rule Drule.beta_eta_conversion);
-
-val mk_head = lift_thm_thy (fn thy => fn thm =>
-  ((CodegenConsts.const_of_cexpr thy o fst o dest_func) thm, thm));
-
-local
-
-exception BAD of string;
-
-fun handle_bad strict thm msg =
-  if strict then error (msg ^ ": " ^ string_of_thm thm)
-    else (warning (msg ^ ": " ^ string_of_thm thm); NONE);
-
-in
+fun assert_func thm =
+  let
+    val thy = Thm.theory_of_thm thm;
+    val args = (snd o strip_comb o fst o Logic.dest_equals
+      o ObjectLogic.drop_judgment thy o Thm.plain_prop_of) thm;
+    val _ =
+      if has_duplicates (op =)
+        ((fold o fold_aterms) (fn Var (v, _) => cons v
+          | _ => I
+        ) args [])
+      then bad_thm ("Duplicated variables on left hand side of equation\n"
+        ^ Display.string_of_thm thm)
+      else ()
+    fun check _ (Abs _) = bad_thm
+          ("Abstraction on left hand side of equation\n"
+            ^ Display.string_of_thm thm)
+      | check 0 (Var _) = ()
+      | check _ (Var _) = bad_thm
+          ("Variable with application on left hand side of defining equation\n"
+            ^ Display.string_of_thm thm)
+      | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
+      | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty
+          then bad_thm
+            ("Partially applied constant on left hand side of equation"
+               ^ Display.string_of_thm thm)
+          else ();
+    val _ = map (check 0) args;
+  in thm end;
 
-fun assert_func strict thm = case try dest_func thm
- of SOME (c_ty as (c, ty), args) => (
-      let
-        val thy = Thm.theory_of_thm thm;
-        val _ =
-          if has_duplicates (op =)
-            ((fold o fold_aterms) (fn Var (v, _) => cons v
-              | _ => I
-            ) args [])
-          then raise BAD "Repeated variables on left hand side of defining equation"
-          else ()
-        fun check _ (Abs _) = raise BAD
-              "Abstraction on left hand side of defining equation"
-          | check 0 (Var _) = ()
-          | check _ (Var _) = raise BAD
-              "Variable with application on left hand side of defining equation"
-          | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
-          | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty
-              then raise BAD
-                ("Partially applied constant on left hand side of defining equation")
-              else ();
-        val _ = map (check 0) args;
-      in SOME thm end handle BAD msg => handle_bad strict thm msg)
-  | NONE => handle_bad strict thm "Not a defining equation";
+val mk_func = assert_func o Drule.fconv_rule Drule.beta_eta_conversion o mk_rew;
 
-end;
-
-fun mk_func strict = map_filter (Option.map mk_head o assert_func strict) o mk_rew;
+fun head_func thm =
+  let
+    val thy = Thm.theory_of_thm thm;
+    val (Const (c_ty as (_, ty))) = (fst o strip_comb o fst o Logic.dest_equals
+      o ObjectLogic.drop_judgment thy o Thm.plain_prop_of) thm;
+    val const = CodegenConsts.const_of_cexpr thy c_ty;
+  in (const, ty) end;
 
 
 (* utilities *)

--- a/src/Pure/Tools/codegen_funcgr.ML	Fri Apr 20 11:21:34 2007 +0200
+++ b/src/Pure/Tools/codegen_funcgr.ML	Fri Apr 20 11:21:35 2007 +0200
@@ -157,9 +157,9 @@
     fun resort_rec tap_typ (const, []) = (true, (const, []))
       | resort_rec tap_typ (const, thms as thm :: _) =
           let
-            val ty = CodegenFunc.typ_func thm;
+            val (_, ty) = CodegenFunc.head_func thm;
             val thms' as thm' :: _ = resort_thms algebra tap_typ thms
-            val ty' = CodegenFunc.typ_func thm';
+            val (_, ty') = CodegenFunc.head_func thm';
           in (Sign.typ_equiv thy (ty, ty'), (const, thms')) end;
     fun resort_recs funcss =
       let
@@ -167,7 +167,7 @@
          of SOME const => AList.lookup (CodegenConsts.eq_const) funcss const
               |> these
               |> try hd
-              |> Option.map CodegenFunc.typ_func
+              |> Option.map (snd o CodegenFunc.head_func)
           | NONE => NONE;
         val (unchangeds, funcss') = split_list (map (resort_rec tap_typ) funcss);
         val unchanged = fold (fn x => fn y => x andalso y) unchangeds true;
@@ -241,10 +241,10 @@
       |> resort_funcss thy algebra funcgr
       |> filter_out (can (Constgraph.get_node funcgr) o fst);
     fun typ_func const [] = CodegenData.default_typ thy const
-      | typ_func (_, NONE) (thm :: _) = CodegenFunc.typ_func thm
+      | typ_func (_, NONE) (thm :: _) = (snd o CodegenFunc.head_func) thm
       | typ_func (const as (c, SOME tyco)) (thms as (thm :: _)) =
           let
-            val ty = CodegenFunc.typ_func thm;
+            val (_, ty) = CodegenFunc.head_func thm;
             val SOME class = AxClass.class_of_param thy c;
             val sorts_decl = Sorts.mg_domain algebra tyco [class];
             val tys = CodegenConsts.typargs thy (c, ty);

--- a/src/Pure/Tools/codegen_package.ML	Fri Apr 20 11:21:34 2007 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Fri Apr 20 11:21:35 2007 +0200
@@ -71,12 +71,22 @@
   fun rewrites thy = [];
 );
 
-fun print_codethms thy =
-  Pretty.writeln o CodegenFuncgr.pretty thy o Funcgr.make thy;
+fun code_depgr thy [] = Funcgr.make thy []
+  | code_depgr thy consts =
+      let
+        val gr = Funcgr.make thy consts;
+        val select = CodegenFuncgr.Constgraph.all_succs gr consts;
+      in
+        CodegenFuncgr.Constgraph.subgraph
+          (member CodegenConsts.eq_const select) gr
+      end;
+
+fun code_thms thy =
+  Pretty.writeln o CodegenFuncgr.pretty thy o code_depgr thy;
 
 fun code_deps thy consts =
   let
-    val gr = Funcgr.make thy consts;
+    val gr = code_depgr thy consts;
     fun mk_entry (const, (_, (_, parents))) =
       let
         val name = CodegenConsts.string_of_const thy const;
@@ -113,7 +123,7 @@
 
 fun prep_eqs thy (thms as thm :: _) =
   let
-    val ty = (Logic.unvarifyT o CodegenFunc.typ_func) thm;
+    val ty = (Logic.unvarifyT o snd o CodegenFunc.head_func) thm;
     val thms' = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
       then thms
       else map (CodegenFunc.expand_eta 1) thms;
@@ -600,34 +610,6 @@
 fun satisfies thy t witnesses = raw_eval_term thy
   (("CodegenPackage.satisfies_ref", satisfies_ref), t) witnesses;
 
-
-(* constant specifications with wildcards *)
-
-fun consts_of thy thyname =
-  let
-    val this_thy = Option.map theory thyname |> the_default thy;
-    val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
-      ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy) [];
-    fun classop c = case AxClass.class_of_param thy c
-     of NONE => [(c, NONE)]
-      | SOME class => Symtab.fold
-          (fn (tyco, classes) => if AList.defined (op =) classes class
-            then cons (c, SOME tyco) else I)
-          ((#arities o Sorts.rep_algebra o Sign.classes_of) this_thy)
-          [(c, NONE)];
-    val consts = maps classop cs;
-    fun test_instance thy (class, tyco) =
-      can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
-    fun belongs_here thyname (c, NONE) =
-          not (exists (fn thy => Sign.declared_const thy c) (Theory.parents_of this_thy))
-      | belongs_here thyname (c, SOME tyco) =
-          not (exists (fn thy => test_instance thy ((the o AxClass.class_of_param thy) c, tyco))
-            (Theory.parents_of this_thy))
-  in case thyname
-   of NONE => consts
-    | SOME thyname => filter (belongs_here thyname) consts
-  end;
-
 fun filter_generatable thy targets consts =
   let
     val (consts', funcgr) = Funcgr.make_consts thy consts;
@@ -636,11 +618,6 @@
       (consts' ~~ consts'');
   in consts''' end;
 
-fun read_constspec thy targets "*" = filter_generatable thy targets (consts_of thy NONE)
-  | read_constspec thy targets s = if String.isSuffix ".*" s
-      then filter_generatable thy targets (consts_of thy (SOME (unsuffix ".*" s)))
-      else [CodegenConsts.read_const thy s];
-
 
 (** toplevel interface and setup **)
 
@@ -655,7 +632,8 @@
           (target, SOME (CodegenSerializer.get_serializer thy target args CodegenNames.labelled_name))
       | (target, []) => (CodegenSerializer.assert_serializer thy target, NONE)) seris;
     val targets = case map fst seris' of [] => NONE | xs => SOME xs;
-    val cs = maps (read_constspec thy targets) raw_cs;
+    val cs = CodegenConsts.read_const_exprs thy
+      (filter_generatable thy targets) raw_cs;
     fun generate' thy = case cs
      of [] => []
       | _ =>
@@ -671,11 +649,11 @@
     (map (serialize' cs code) (map_filter snd seris'); ())
   end;
 
-fun print_codethms_cmd thy =
-  print_codethms thy o map (CodegenConsts.read_const thy);
+fun code_thms_cmd thy =
+  code_thms thy o CodegenConsts.read_const_exprs thy (fst o Funcgr.make_consts thy);
 
 fun code_deps_cmd thy =
-  code_deps thy o map (CodegenConsts.read_const thy);
+  code_deps thy o CodegenConsts.read_const_exprs thy (fst o Funcgr.make_consts thy);
 
 val code_exprP = (
     (Scan.repeat P.term
@@ -713,13 +691,13 @@
   );
 
 val code_thmsP =
-  OuterSyntax.improper_command code_thmsK "print cached defining equations" OuterKeyword.diag
+  OuterSyntax.improper_command code_thmsK "print system of defining equations for code" OuterKeyword.diag
     (Scan.repeat P.term
       >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
-        o Toplevel.keep ((fn thy => print_codethms_cmd thy cs) o Toplevel.theory_of)));
+        o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
 
 val code_depsP =
-  OuterSyntax.improper_command code_depsK "visualize dependencies of defining equations" OuterKeyword.diag
+  OuterSyntax.improper_command code_depsK "visualize dependencies of defining equations for code" OuterKeyword.diag
     (Scan.repeat P.term
       >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
         o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));