# HG changeset patch
# User haftmann
# Date 1159822851 -7200
# Node ID 27d049062b560f2fc5e85459c5bdd2ab63d290ef
# Parent  9a24a9121e58b0dab713bc0ece6c3dff51a3ad4b
tuned

diff -r 9a24a9121e58 -r 27d049062b56 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Mon Oct 02 23:00:50 2006 +0200
+++ b/src/HOL/Integ/NatBin.thy	Mon Oct 02 23:00:51 2006 +0200
@@ -790,7 +790,7 @@
 
 val nat_number_expand = thms "nat_number_expand";
 
-fun elim_number_of_nat thy thms =
+fun elim_number_of_nat thy ts =
   let
     fun bins_of (Const _) =
           I
@@ -809,22 +809,19 @@
             | (t', ts) => bins_of t' #> fold bins_of ts;
     val simpset =
       HOL_basic_ss addsimps nat_number_expand;
-    val rewrites  =
-      []
-      |> (fold o Drule.fold_terms) bins_of thms
-      |> map (Simplifier.rewrite simpset o Thm.cterm_of thy);
-  in if null rewrites then thms else
-    map (CodegenData.rewrite_func rewrites) thms
+  in
+    []
+    |> fold (bins_of o Thm.term_of) ts
+    |> map (Simplifier.rewrite simpset o Thm.cterm_of thy)
   end;
 
 end;
 *}
 
 setup {*
-  CodegenData.add_preproc NumeralNat.elim_number_of_nat
+  CodegenData.add_inline_proc NumeralNat.elim_number_of_nat
 *}
 
-
 subsection {* legacy ML bindings *}
 
 ML
diff -r 9a24a9121e58 -r 27d049062b56 src/HOL/OperationalEquality.thy
--- a/src/HOL/OperationalEquality.thy	Mon Oct 02 23:00:50 2006 +0200
+++ b/src/HOL/OperationalEquality.thy	Mon Oct 02 23:00:51 2006 +0200
@@ -18,17 +18,6 @@
 defs
   eq_def: "eq x y \<equiv> (x = y)"
 
-ML {*
-local
-  val thy = the_context ();
-  val const_eq = Sign.intern_const thy "eq";
-  val type_bool = Type (Sign.intern_type thy "bool", []);
-in
-  val eq_def_sym = Thm.symmetric (thm "eq_def");
-  val class_eq = Sign.intern_class thy "eq";
-end
-*}
-
 
 subsection {* bool type *}
 
@@ -47,31 +36,24 @@
   "eq p False = (\<not> p)" unfolding eq_def by auto
 
 
-subsection {* preprocessor *}
+subsection {* code generator setup *}
 
-ML {*
-fun constrain_op_eq thy thms =
-  let
-    fun add_eq (Const ("op =", ty)) =
-          fold (insert (eq_fst (op = : indexname * indexname -> bool)))
-            (Term.add_tvarsT ty [])
-      | add_eq _ =
-          I
-    val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
-    val instT = map (fn (v_i, sort) =>
-      (Thm.ctyp_of thy (TVar (v_i, sort)),
-         Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [class_eq]))))) eqs;
-  in
-    thms
-    |> map (Thm.instantiate (instT, []))
-  end;
-*}
-
-
-subsection {* codegenerator setup *}
+subsubsection {* preprocessor *}
 
 setup {*
-  CodegenData.add_preproc constrain_op_eq
+let
+  val class_eq = "OperationalEquality.eq";
+  fun constrain_op_eq thy ts =
+    let
+      fun add_eq (Const ("op =", ty)) =
+            fold (insert (eq_fst (op = : indexname * indexname -> bool)))
+              (Term.add_tvarsT ty [])
+        | add_eq _ =
+            I
+      val eqs = (fold o fold_aterms) add_eq ts [];
+      val inst = map (fn (v_i, _) => (v_i, [class_eq])) eqs;
+    in inst end;
+in CodegenData.add_constrains constrain_op_eq end
 *}
 
 declare eq_def [symmetric, code inline]
diff -r 9a24a9121e58 -r 27d049062b56 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Mon Oct 02 23:00:50 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Mon Oct 02 23:00:51 2006 +0200
@@ -9,10 +9,8 @@
 sig
   val get_eq: theory -> string -> thm list
   val get_eq_datatype: theory -> string -> thm list
-  val get_eq_typecopy: theory -> string -> thm list
   val get_cert: theory -> bool * string -> thm list
   val get_cert_datatype: theory -> string -> thm list
-  val get_cert_typecopy: theory -> string -> thm list
   val dest_case_expr: theory -> term
     -> ((string * typ) list * ((term * typ) * (term * term) list)) option
   val add_datatype_case_const: string -> theory -> theory
@@ -29,11 +27,13 @@
   val get_codetypes_arities: theory -> (string * bool) list -> sort
     -> (string * (((string * sort list) * sort) * term list)) list option
   val prove_codetypes_arities: (thm list -> tactic) -> (string * bool) list -> sort
-    -> (theory -> ((string * sort list) * sort) list -> (string * term list) list
-    -> ((bstring * attribute list) * term) list) -> (theory -> theory) -> theory -> theory
+    -> (((string * sort list) * sort) list -> (string * term list) list -> theory
+    -> ((bstring * attribute list) * term) list * theory)
+    -> (((string * sort list) * sort) list -> (string * term list) list -> theory -> theory)
+    -> theory -> theory
 
   val setup: theory -> theory
-  val setup2: theory -> theory
+  val setup_hooks: theory -> theory
 end;
 
 structure DatatypeCodegen : DATATYPE_CODEGEN =
@@ -364,7 +364,7 @@
         val names = Name.invents ctxt "a" (length tys);
         val ctxt' = fold Name.declare names ctxt;
         val vs = map2 (curry Free) names tys;
-      in (vs, ctxt) end;
+      in (vs, ctxt') end;
     fun mk_dist ((co1, tys1), (co2, tys2)) =
       let
         val ((xs1, xs2), _) = Name.context
@@ -400,17 +400,39 @@
       |> map (fn t => Goal.prove_global thy [] [] t (K tac))
       |> map (fn thm => not_eq_quodlibet OF [thm])
   in inject @ distinct end
-and get_cert_typecopy thy dtco =
-  let
-    val SOME { inject, ... } = TypecopyPackage.get_typecopy_info thy dtco;
-    val thm = Tactic.rewrite_rule [rew_eq] (bool_eq_implies OF [inject]);
-  in
-    [thm]
-  end;
 end (*local*);
 
-fun get_cert thy (true, dtco) = get_cert_datatype thy dtco
-  | get_cert thy (false, dtco) = get_cert_typecopy thy dtco;
+local
+  val not_sym = thm "HOL.not_sym";
+  val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
+in fun get_eq_datatype thy dtco =
+  let
+    val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
+    fun mk_triv_inject co =
+      let
+        val ct' = Thm.cterm_of thy
+          (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs)))
+        val cty' = Thm.ctyp_of_term ct';
+        val refl = Thm.prop_of HOL.refl;
+        val SOME (ct, cty) = fold_aterms (fn Var (v, ty) =>
+          (K o SOME) (Thm.cterm_of thy (Var (v, Thm.typ_of cty')), Thm.ctyp_of thy ty) | _ => I)
+          refl NONE;
+      in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
+    val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
+    val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco;
+    val ctxt = Context.init_proof thy;
+    val simpset = Simplifier.context ctxt
+      (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
+    val cos = map (fn (co, tys) =>
+        (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
+    val tac = ALLGOALS (simp_tac simpset)
+      THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]);
+    val distinct =
+      mk_distinct cos
+      |> map (fn t => Goal.prove_global thy [] [] t (K tac))
+      |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
+  in inject1 @ inject2 @ distinct end;
+end (*local*);
 
 fun add_datatype_case_const dtco thy =
   let
@@ -429,8 +451,7 @@
 
 (** codetypes for code 2nd generation **)
 
-type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
-  -> theory -> theory;
+(* abstraction over datatypes vs. type copies *)
 
 fun codetypes_dependency thy =
   let
@@ -461,23 +482,54 @@
     |> map (AList.make (the o AList.lookup (op =) names))
   end;
 
-fun mk_typecopy_spec ({ vs, constr, typ, ... } : TypecopyPackage.info) =
-  (vs, [(constr, [typ])]);
-
 fun get_spec thy (dtco, true) =
       (the o DatatypePackage.get_datatype_spec thy) dtco
   | get_spec thy (tyco, false) =
-      (mk_typecopy_spec o the o TypecopyPackage.get_typecopy_info thy) tyco;
+      TypecopyPackage.get_spec thy tyco;
+
+fun get_cert thy (true, dtco) = get_cert_datatype thy dtco
+  | get_cert thy (false, dtco) = [TypecopyPackage.get_cert thy dtco];
 
-fun add_spec thy (tyco, is_dt) =
-  (tyco, (is_dt, get_spec thy (tyco, is_dt)));
+local
+  val eq_def_sym = thm "eq_def" |> Thm.symmetric;
+  val class_eq = "OperationalEquality.eq";
+  fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
+   of SOME _ => get_eq_datatype thy tyco
+    | NONE => [TypecopyPackage.get_eq thy tyco];
+  fun constrain_op_eq_thms thy thms =
+    let
+      fun add_eq (Const ("op =", ty)) =
+            fold (insert (eq_fst (op =)))
+              (Term.add_tvarsT ty [])
+        | add_eq _ =
+            I
+      val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
+      val instT = map (fn (v_i, sort) =>
+        (Thm.ctyp_of thy (TVar (v_i, sort)),
+           Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [class_eq]))))) eqs;
+    in
+      thms
+      |> map (Thm.instantiate (instT, []))
+    end;
+in
+  fun get_eq thy tyco =
+    get_eq_thms thy tyco
+    |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy)
+    |> constrain_op_eq_thms thy
+    |> map (Tactic.rewrite_rule [eq_def_sym])
+end;
+
+type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
+  -> theory -> theory;
 
 fun add_codetypes_hook_bootstrap hook thy =
   let
+    fun add_spec thy (tyco, is_dt) =
+      (tyco, (is_dt, get_spec thy (tyco, is_dt)));
     fun datatype_hook dtcos thy =
       hook (map (add_spec thy) (map (rpair true) dtcos)) thy;
-    fun typecopy_hook ((tyco, info )) thy =
-      hook ([(tyco, (false, mk_typecopy_spec info))]) thy;
+    fun typecopy_hook ((tyco, _)) thy =
+      hook ([(tyco, (false, TypecopyPackage.get_spec thy tyco))]) thy;
   in
     thy
     |> fold hook ((map o map) (add_spec thy) (codetypes_dependency thy))
@@ -498,6 +550,23 @@
         val (vs::_, css) = split_list (map (the o DatatypePackage.get_datatype_spec thy) tycos);
       in (vs, map2 (fn (tyco, is_dt) => fn cs => (tyco, (is_dt, cs))) tycos' css) end;
 
+
+(* registering code types in code generator *)
+
+fun codetype_hook specs =
+  let
+    fun add (dtco, (flag, spec)) thy =
+      let
+        fun cert thy_ref = (fn () => get_cert (Theory.deref thy_ref) (flag, dtco));
+      in
+        CodegenData.add_datatype
+          (dtco, (spec, CodegenData.lazy (cert (Theory.self_ref thy)))) thy
+      end;
+  in fold add specs end;
+
+
+(* instrumentalizing the sort algebra *)
+
 fun get_codetypes_arities thy tycos sort =
   let
     val algebra = Sign.classes_of thy;
@@ -538,114 +607,35 @@
             then NONE else SOME (arity, (tyco, cs)))) insts;
       in
         thy
-        |> K ((not o null) arities) ? (ClassPackage.prove_instance_arity tac
-             arities ("", []) (f thy arities css) #> after_qed)
+        |> K ((not o null) arities) ? (
+            f arities css
+            #-> (fn defs =>
+              ClassPackage.prove_instance_arity tac arities ("", []) defs
+            #> after_qed arities css))
       end;
 
+
+(* operational equality *)
+
 local
   val class_eq = "OperationalEquality.eq";
-in fun add_eq_instance specs =
-  prove_codetypes_arities
-    (K (ClassPackage.intro_classes_tac []))
-    (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
-    [class_eq] ((K o K o K) [])
-end; (*local*)
-
-local
-  val not_sym = thm "HOL.not_sym";
-  val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
-in fun get_eq_datatype thy dtco =
+in fun eq_hook specs =
   let
-(*     val _ = writeln "01";  *)
-    val SOME (vs, cs) = DatatypePackage.get_datatype_spec (Context.check_thy thy) dtco;
-(*     val _ = writeln "02";  *)
-    fun mk_triv_inject co =
+    fun add_eq_thms (dtco, (_, (vs, cs))) thy =
       let
-        val ct' = Thm.cterm_of (Context.check_thy thy)
-          (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs)))
-        val cty' = Thm.ctyp_of_term ct';
-        val refl = Thm.prop_of HOL.refl;
-        val SOME (ct, cty) = fold_aterms (fn Var (v, ty) =>
-          (K o SOME) (Thm.cterm_of (Context.check_thy thy) (Var (v, Thm.typ_of cty')), Thm.ctyp_of (Context.check_thy thy) ty) | _ => I)
-          refl NONE;
-      in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
-(*     val _ = writeln "03";  *)
-    val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
-(*     val _ = writeln "04";  *)
-    val inject2 = (#inject o DatatypePackage.the_datatype (Context.check_thy thy)) dtco;
-(*     val _ = writeln "05";  *)
-    val ctxt = Context.init_proof (Context.check_thy thy);
-(*     val _ = writeln "06";  *)
-    val simpset = Simplifier.context ctxt
-      (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
-(*     val _ = writeln "07";  *)
-    val cos = map (fn (co, tys) =>
-        (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
-    val tac = ALLGOALS (simp_tac simpset)
-      THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]);
-(*     val _ = writeln "08";  *)
-    val distinct =
-      mk_distinct cos
-      |> map (fn t => Goal.prove_global (Context.check_thy thy) [] [] t (K tac))
-      |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
-(*     val _ = writeln "09";  *)
-  in inject1 @ inject2 @ distinct end;
-
-fun get_eq_typecopy thy tyco =
-  case TypecopyPackage.get_typecopy_info thy tyco
-   of SOME { inject, ... } => [inject]
-    | NONE => [];
-
-local
-  val lift_not_thm = thm "HOL.Eq_FalseI";
-  val lift_thm = thm "HOL.eq_reflection";
-  val eq_def_sym = thm "eq_def" |> Thm.symmetric;
-  fun get_eq_thms thy tyco = case DatatypePackage.get_datatype (Context.check_thy thy) tyco
-   of SOME _ => get_eq_datatype (Context.check_thy thy) tyco
-    | NONE => case TypecopyPackage.get_typecopy_info thy tyco
-       of SOME _ => get_eq_typecopy thy tyco
-        | NONE => [];
-in
-  fun get_eq thy tyco =
-    get_eq_thms (Context.check_thy thy) tyco
-(*     |> tap (fn _ => writeln "10")  *)
-    |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) (Context.check_thy thy))
-(*     |> tap (fn _ => writeln "11")  *)
-    |> constrain_op_eq (Context.check_thy thy)
-(*     |> tap (fn _ => writeln "12")  *)
-    |> map (Tactic.rewrite_rule [eq_def_sym])
-(*     |> tap (fn _ => writeln "13")  *)
-end;
-
-end;
-
-fun add_eq_thms (dtco, (_, (vs, cs))) thy =
-  let
-    val thy_ref = Theory.self_ref thy;
-    val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
-    val c = CodegenConsts.norm thy ("OperationalEquality.eq", [ty]);
-    val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
-  in
-    CodegenData.add_funcl
-      (c, CodegenData.lazy get_thms) thy
-  end;
-
-fun codetype_hook dtcos theory =
-  let
-    fun add (dtco, (flag, spec)) thy =
-      let
-        fun cert thy_ref = (fn () => get_cert (Theory.deref thy_ref) (flag, dtco));
+        val thy_ref = Theory.self_ref thy;
+        val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
+        val c = CodegenConsts.norm thy ("OperationalEquality.eq", [ty]);
+        val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
       in
-        CodegenData.add_datatype
-          (dtco, (spec, CodegenData.lazy (cert (Theory.self_ref thy)))) thy
+        CodegenData.add_funcl (c, CodegenData.lazy get_thms) thy
       end;
   in
-    theory
-    |> fold add dtcos
+    prove_codetypes_arities (K (ClassPackage.intro_classes_tac []))
+      (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
+      [class_eq] ((K o K o pair) []) ((K o K) (fold add_eq_thms specs))
   end;
-
-fun eq_hook dtcos =
-  add_eq_instance dtcos (fold add_eq_thms dtcos);
+end; (*local*)
 
 
 
@@ -657,7 +647,7 @@
   #> DatatypeHooks.add (fold add_datatype_case_const)
   #> DatatypeHooks.add (fold add_datatype_case_defs)
 
-val setup2 =
+val setup_hooks =
   add_codetypes_hook_bootstrap codetype_hook
   #> add_codetypes_hook_bootstrap eq_hook
 
diff -r 9a24a9121e58 -r 27d049062b56 src/HOL/Tools/typecopy_package.ML
--- a/src/HOL/Tools/typecopy_package.ML	Mon Oct 02 23:00:50 2006 +0200
+++ b/src/HOL/Tools/typecopy_package.ML	Mon Oct 02 23:00:51 2006 +0200
@@ -19,8 +19,11 @@
     -> theory -> (string * info) * theory
   val get_typecopies: theory -> string list
   val get_typecopy_info: theory -> string -> info option
-  type hook = string * info -> theory -> theory;
-  val add_hook: hook -> theory -> theory;
+  type hook = string * info -> theory -> theory
+  val add_hook: hook -> theory -> theory
+  val get_spec: theory -> string -> (string * sort) list * (string * typ list) list
+  val get_cert: theory -> string -> thm
+  val get_eq: theory -> string -> thm
   val print: theory -> unit
   val setup: theory -> theory
 end;
@@ -134,7 +137,28 @@
 end; (*local*)
 
 
-(* hooks for projection function code *)
+(* equality function equation *)
+
+fun get_eq thy tyco =
+  (#inject o the o get_typecopy_info thy) tyco;
+
+
+(* datatype specification and certificate *)
+
+fun get_spec thy tyco =
+  let
+    val SOME { vs, constr, typ, ... } = get_typecopy_info thy tyco
+  in (vs, [(constr, [typ])]) end;
+
+local
+  val bool_eq_implies = thm "iffD1";
+  val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric;
+in fun get_cert thy tyco =
+  Tactic.rewrite_rule [rew_eq] (bool_eq_implies OF [get_eq thy tyco])
+end; (*local*)
+
+
+(* hook for projection function code *)
 
 fun add_project (_ , { proj_def, ...} : info) =
   CodegenData.add_func proj_def;
diff -r 9a24a9121e58 -r 27d049062b56 src/HOL/ex/CodeEval.thy
--- a/src/HOL/ex/CodeEval.thy	Mon Oct 02 23:00:50 2006 +0200
+++ b/src/HOL/ex/CodeEval.thy	Mon Oct 02 23:00:51 2006 +0200
@@ -39,15 +39,14 @@
 
 setup {*
 let
-  fun mk thy arities _ =
-    maps (fn ((tyco, asorts), _) => [(("", []), TypOf.mk_typ_of_def
-      (Type (tyco, map TFree (Name.names Name.context "'a" asorts)))
-      |> tap (writeln o Sign.string_of_term thy))]) arities;
+  fun mk arities _ thy =
+    (maps (fn ((tyco, asorts), _) => [(("", []), TypOf.mk_typ_of_def
+      (Type (tyco, map TFree (Name.names Name.context "'a" asorts))))]) arities, thy);
   fun tac _ = ClassPackage.intro_classes_tac [];
   fun hook specs =
     DatatypeCodegen.prove_codetypes_arities tac
       (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
-      [TypOf.class_typ_of] mk I
+      [TypOf.class_typ_of] mk ((K o K) I)
 in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
 *}
 
@@ -90,19 +89,27 @@
 
 setup {*
 let
-  fun mk thy arities css =
+  fun thy_note ((name, atts), thms) =
+    PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
+  fun thy_def ((name, atts), t) =
+    PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
+  fun mk arities css thy =
     let
       val vs = (Name.names Name.context "'a" o snd o fst o hd) arities;
-      val raw_defs = map (TermOf.mk_terms_of_defs vs) css;
-      fun mk' thy' = map (apfst (rpair [])) ((PrimrecPackage.mk_combdefs thy' o flat) raw_defs)
-    in ClassPackage.assume_arities_thy thy arities mk' end;
+      val defs = map (TermOf.mk_terms_of_defs vs) css;
+      val defs' = (map (pair ("", []) o ObjectLogic.ensure_propT thy) o flat) defs;
+    in
+      thy
+      |> PrimrecPackage.gen_primrec thy_note thy_def "" defs'
+      |> snd
+    end;
   fun tac _ = ClassPackage.intro_classes_tac [];
   fun hook specs =
     if (fst o hd) specs = (fst o dest_Type) Embed.typ_typ then I
     else
       DatatypeCodegen.prove_codetypes_arities tac
       (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
-      [TermOf.class_term_of] mk I
+      [TermOf.class_term_of] ((K o K o pair) []) mk
 in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
 *}
 
diff -r 9a24a9121e58 -r 27d049062b56 src/Pure/Tools/codegen_funcgr.ML
--- a/src/Pure/Tools/codegen_funcgr.ML	Mon Oct 02 23:00:50 2006 +0200
+++ b/src/Pure/Tools/codegen_funcgr.ML	Mon Oct 02 23:00:51 2006 +0200
@@ -9,9 +9,10 @@
 sig
   type T;
   val mk_funcgr: theory -> CodegenConsts.const list -> (string * typ) list -> T
+  val all_deps_of: T -> CodegenConsts.const list -> CodegenConsts.const list list
   val get_funcs: T -> CodegenConsts.const -> thm list
   val get_func_typs: T -> (CodegenConsts.const * typ) list
-  val preprocess: theory -> thm list -> thm list
+  val normalize: theory -> thm list -> thm list
   val print_codethms: theory -> CodegenConsts.const list -> unit
 end;
 
@@ -98,7 +99,7 @@
     val (_, _, inst) = fold mk_inst (vars_of thm) (maxidx + 1, [], []);
   in Thm.instantiate ([], inst) thm end;
 
-fun preprocess thy thms =
+fun normalize thy thms =
   let
     fun burrow_thms f [] = []
       | burrow_thms f thms =
@@ -110,7 +111,6 @@
       #2 (#1 (Variable.import true thms (ProofContext.init thy)));
   in
     thms
-    |> CodegenData.preprocess thy
     |> map (abs_norm thy)
     |> burrow_thms (
         canonical_tvars thy
@@ -119,43 +119,25 @@
        )
   end;
 
-fun check_thms c thms =
-  let
-    fun check_head_lhs thm (lhs, rhs) =
-      case strip_comb lhs
-       of (Const (c', _), _) => if c' = c then ()
-           else error ("Illegal function equation for " ^ quote c
-             ^ ", actually defining " ^ quote c' ^ ": " ^ Display.string_of_thm thm)
-        | _ => error ("Illegal function equation: " ^ Display.string_of_thm thm);
-    fun check_vars_lhs thm (lhs, rhs) =
-      if has_duplicates (op =)
-          (fold_aterms (fn Free (v, _) => cons v | _ => I) lhs [])
-      then error ("Repeated variables on left hand side of function equation:"
-        ^ Display.string_of_thm thm)
-      else ();
-    fun check_vars_rhs thm (lhs, rhs) =
-      if null (subtract (op =)
-        (fold_aterms (fn Free (v, _) => cons v | _ => I) lhs [])
-        (fold_aterms (fn Free (v, _) => cons v | _ => I) rhs []))
-      then ()
-      else error ("Free variables on right hand side of function equation:"
-        ^ Display.string_of_thm thm)
-    val tts = map (Logic.dest_equals o Logic.unvarify o Thm.prop_of) thms;
-  in
-    (map2 check_head_lhs thms tts; map2 check_vars_lhs thms tts;
-      map2 check_vars_rhs thms tts; thms)
-  end;
-
 
 
 (** retrieval **)
 
 fun get_funcs funcgr (c_tys as (c, _)) =
-  (check_thms c o these o Option.map snd o try (Constgraph.get_node funcgr)) c_tys;
+  (these o Option.map snd o try (Constgraph.get_node funcgr)) c_tys;
 
 fun get_func_typs funcgr =
   AList.make (fst o Constgraph.get_node funcgr) (Constgraph.keys funcgr);
 
+fun all_deps_of funcgr cs =
+  let
+    val conn = Constgraph.strong_conn funcgr;
+    val order = rev conn;
+  in
+    (map o filter) (member (op =) (Constgraph.all_succs funcgr cs)) order
+    |> filter_out null
+  end;
+
 local
 
 fun add_things_of thy f (c, thms) =
@@ -234,7 +216,7 @@
     |> Constgraph.new_node (c, [])
     |> pair (SOME c)
   else let
-    val thms = preprocess thy (CodegenData.these_funcs thy c);
+    val thms = normalize thy (CodegenData.these_funcs thy c);
     val rhs = rhs_of thy (c, thms);
   in
     auxgr
diff -r 9a24a9121e58 -r 27d049062b56 src/Pure/Tools/codegen_names.ML
--- a/src/Pure/Tools/codegen_names.ML	Mon Oct 02 23:00:50 2006 +0200
+++ b/src/Pure/Tools/codegen_names.ML	Mon Oct 02 23:00:51 2006 +0200
@@ -236,33 +236,7 @@
 
 (* explicit given names with cache update *)
 
-fun tyco_force (tyco, name) thy =
-  let
-    val names = NameSpace.unpack name;
-    val (prefix, base) = split_last (NameSpace.unpack name);
-    val prefix' = purify_prefix prefix;
-    val base' = purify_base base;
-    val _ = if (base' = base) andalso forall (op =) (prefix' ~~ prefix)
-      then ()
-      else
-        error ("Name violates naming conventions: " ^ quote name
-          ^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base'])))
-    val names_ref = CodeName.get thy;
-    val (Names names) = ! names_ref;
-    val (tycotab, tycorev) = #tyco names;
-    val _ = if Symtab.defined tycotab tyco
-      then error ("Type constructor already named: " ^ quote tyco)
-      else ();
-    val _ = if Symtab.defined tycorev name
-      then error ("Name already given to type constructor: " ^ quote name)
-      else ();
-    val _ = names_ref := map_tyco (K (Symtab.update_new (tyco, name) tycotab,
-          Symtab.update_new (name, tyco) tycorev)) (Names names);
-  in
-    thy
-  end;
-
-fun const_force (c_tys as (c, _), name) thy =
+fun force get defined upd_names upd errname string_of (x, name) thy =
   let
     val names = NameSpace.unpack name;
     val (prefix, base) = split_last (NameSpace.unpack name);
@@ -275,44 +249,25 @@
           ^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base'])))
     val names_ref = CodeName.get thy;
     val (Names names) = ! names_ref;
-    val (const, constrev) = #const names;
-    val _ = if Consttab.defined const c_tys
-      then error ("Constant already named: " ^ quote (CodegenConsts.string_of_const thy c_tys))
+    val (tab, rev) = get names;
+    val _ = if defined tab x
+      then error ("Already named " ^ errname  ^ ": " ^ string_of thy x)
       else ();
-    val _ = if Symtab.defined constrev name
-      then error ("Name already given to constant: " ^ quote name)
+    val _ = if Symtab.defined rev name
+      then error ("Name already given to other " ^ errname ^ ": " ^ quote name)
       else ();
-    val _ = names_ref := map_const (K (Consttab.update_new (c_tys, name) const,
-          Symtab.update_new (name, c_tys) constrev)) (Names names);
+    val _ = names_ref := upd_names (K (upd (x, name) tab,
+          Symtab.update_new (name, x) rev)) (Names names);
   in
     thy
   end;
 
-fun instance_force (instance, name) thy =
-  let
-    val names = NameSpace.unpack name;
-    val (prefix, base) = split_last (NameSpace.unpack name);
-    val prefix' = purify_prefix prefix;
-    val base' = purify_base base;
-    val _ = if (base' = base) andalso forall (op =) (prefix' ~~ prefix)
-      then ()
-      else
-        error ("Name violates naming conventions: " ^ quote name
-          ^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base'])))
-    val names_ref = CodeName.get thy;
-    val (Names names) = ! names_ref;
-    val (inst, instrev) = #instance names;
-    val _ = if Insttab.defined inst instance
-      then error ("Instance already named: " ^ quote (fst instance) ^ ", " ^ quote (snd instance))
-      else ();
-    val _ = if Symtab.defined instrev name
-      then error ("Name already given to instance: " ^ quote name)
-      else ();
-    val _ = names_ref := map_inst (K (Insttab.update_new (instance, name) inst,
-          Symtab.update_new (name, instance) instrev)) (Names names);
-  in
-    thy
-  end;
+val tyco_force = force #tyco Symtab.defined map_tyco Symtab.update_new
+  "type constructor" (K quote);
+val instance_force = force #instance Insttab.defined map_inst Insttab.update_new
+  "instance" (fn _ => fn (class, tyco) => quote class ^ ", " ^ quote tyco);
+val const_force = force #const Consttab.defined map_const Consttab.update_new
+  "constant" (quote oo CodegenConsts.string_of_const);
 
 
 (* naming policies *)
@@ -442,21 +397,21 @@
 val (constnameK, typenameK, instnameK) = ("code_constname", "code_typename", "code_instname");
 
 val constnameP =
-  OuterSyntax.command constnameK "declare code name for constant" K.thy_decl (
+  OuterSyntax.improper_command constnameK "declare code name for constant" K.thy_decl (
     Scan.repeat1 (P.term -- P.name)
     >> (fn aliasses =>
           Toplevel.theory (fold const_force_e aliasses))
   );
 
 val typenameP =
-  OuterSyntax.command typenameK "declare code name for type constructor" K.thy_decl (
+  OuterSyntax.improper_command typenameK "declare code name for type constructor" K.thy_decl (
     Scan.repeat1 (P.xname -- P.name)
     >> (fn aliasses =>
           Toplevel.theory (fold tyco_force_e aliasses))
   );
 
 val instnameP =
-  OuterSyntax.command instnameK "declare code name for instance relation" K.thy_decl (
+  OuterSyntax.improper_command instnameK "declare code name for instance relation" K.thy_decl (
     Scan.repeat1 ((P.xname --| P.$$$ "::" -- P.xname) -- P.name)
     >> (fn aliasses =>
           Toplevel.theory (fold instance_force_e aliasses))
diff -r 9a24a9121e58 -r 27d049062b56 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Mon Oct 02 23:00:50 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Mon Oct 02 23:00:51 2006 +0200
@@ -16,7 +16,6 @@
 
   type appgen;
   val add_appconst: string * appgen -> theory -> theory;
-  val appgen_default: appgen;
   val appgen_numeral: (theory -> term -> IntInf.int) -> appgen;
   val appgen_char: (term -> int option) -> appgen;
   val appgen_case: (theory -> term
@@ -101,8 +100,6 @@
   | check_strict has_seri x (true, _) =
       true;
 
-fun no_strict (_, targets) = (false, targets);
-
 fun ensure_def_class thy algbr funcgr strct cls trns =
   let
     fun defgen_class thy (algbr as ((proj_sort, _), _)) funcgr strct cls trns =
@@ -114,7 +111,7 @@
               val idfs = map (CodegenNames.const thy o CodegenConsts.norm_of_typ thy) cs;
             in
               trns
-              |> debug_msg (fn _ => "trying defgen class declaration for " ^ quote cls)
+              |> tracing (fn _ => "trying defgen class declaration for " ^ quote cls)
               |> fold_map (ensure_def_class thy algbr funcgr strct) superclasses
               ||>> (fold_map (exprgen_type thy algbr funcgr strct) o map snd) cs
               |-> (fn (supcls, memtypes) => succeed
@@ -126,7 +123,7 @@
     val cls' = CodegenNames.class thy cls;
   in
     trns
-    |> debug_msg (fn _ => "generating class " ^ quote cls)
+    |> tracing (fn _ => "generating class " ^ quote cls)
     |> ensure_def (defgen_class thy algbr funcgr strct) true ("generating class " ^ quote cls) cls'
     |> pair cls'
   end
@@ -140,7 +137,7 @@
          (case CodegenData.get_datatype thy dtco
              of SOME (vs, cos) =>
                   trns
-                  |> debug_msg (fn _ => "trying defgen datatype for " ^ quote dtco)
+                  |> tracing (fn _ => "trying defgen datatype for " ^ quote dtco)
                   |> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
                   ||>> fold_map (fn (c, tys) =>
                     fold_map (exprgen_type thy algbr funcgr strct) tys
@@ -156,7 +153,7 @@
             |> fail ("Not a type constructor: " ^ quote dtco)
   in
     trns
-    |> debug_msg (fn _ => "generating type constructor " ^ quote tyco)
+    |> tracing (fn _ => "generating type constructor " ^ quote tyco)
     |> ensure_def (defgen_datatype thy algbr funcgr strct) strict
         ("generating type constructor " ^ quote tyco) tyco'
     |> pair tyco'
@@ -182,7 +179,7 @@
       ||>> fold_map (exprgen_type thy algbr funcgr strct) tys
       |-> (fn (tyco, tys) => pair (tyco `%% tys));
 
-exception CONSTRAIN of ((string * typ) * typ) * term option;
+exception CONSTRAIN of (string * typ) * typ;
 
 fun exprgen_typinst thy (algbr as ((proj_sort, algebra), consts)) funcgr strct (ty_ctxt, sort_decl) trns =
   let
@@ -225,7 +222,7 @@
     val insts = (op ~~ o apsnd (map (snd o dest_TVar)) oo pairself)
       (curry (Consts.typargs consts) idf) (ty_ctxt, ty_decl);
     val _ = if exists not (map (Sign.of_sort thy) insts)
-      then raise CONSTRAIN (((c, ty_decl), ty_ctxt), NONE) else ();
+      then raise CONSTRAIN ((c, ty_decl), ty_ctxt) else ();
   in
     trns
     |> fold_map (exprgen_typinst thy algbr funcgr strct) insts
@@ -251,7 +248,7 @@
                 ||>> exprgen_term thy algbr funcgr strct (Const (m, ty));
             in
               trns
-              |> debug_msg (fn _ => "trying defgen class instance for (" ^ quote cls
+              |> tracing (fn _ => "trying defgen class instance for (" ^ quote cls
                    ^ ", " ^ quote tyco ^ ")")
               |> ensure_def_class thy algbr funcgr strct class
               ||>> ensure_def_tyco thy algbr funcgr strct tyco
@@ -266,7 +263,7 @@
     val inst = CodegenNames.instance thy (cls, tyco);
   in
     trns
-    |> debug_msg (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco)
+    |> tracing (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco)
     |> ensure_def (defgen_inst thy algbr funcgr strct) true
          ("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst
     |> pair inst
@@ -277,7 +274,7 @@
       case CodegenData.get_datatype_of_constr thy ((the o CodegenNames.const_rev thy) co)
        of SOME tyco =>
             trns
-            |> debug_msg (fn _ => "trying defgen datatype constructor for " ^ quote co)
+            |> tracing (fn _ => "trying defgen datatype constructor for " ^ quote co)
             |> ensure_def_tyco thy algbr funcgr strct tyco
             |-> (fn _ => succeed Bot)
         | _ =>
@@ -288,7 +285,7 @@
       case AxClass.class_of_param thy ((fst o the o CodegenNames.const_rev thy) m)
        of SOME class =>
             trns
-            |> debug_msg (fn _ => "trying defgen class operation for " ^ quote m)
+            |> tracing (fn _ => "trying defgen class operation for " ^ quote m)
             |> ensure_def_class thy algbr funcgr strct class
             |-> (fn _ => succeed Bot)
         | _ =>
@@ -300,28 +297,16 @@
               val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms);
               val ty = (Logic.unvarifyT o CodegenData.typ_func thy) eq_thm;
               val vs = (map dest_TFree o Consts.typargs consts) (c', ty);
-              fun dest_eqthm eq_thm =
-                let
-                  val ((t, args), rhs) =
-                    (apfst strip_comb o Logic.dest_equals o Logic.unvarify o prop_of) eq_thm;
-                in case t
-                 of Const (c', _) => if c' = c then (args, rhs)
-                     else error ("Illegal function equation for " ^ quote c
-                       ^ ", actually defining " ^ quote c')
-                  | _ => error ("Illegal function equation for " ^ quote c)
-                end;
+              val dest_eqthm =
+                apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify o prop_of;
               fun exprgen_eq (args, rhs) trns =
                 trns
                 |> fold_map (exprgen_term thy algbr funcgr strct) args
                 ||>> exprgen_term thy algbr funcgr strct rhs;
-              fun checkvars (args, rhs) =
-                if CodegenThingol.vars_distinct args then (args, rhs)
-                else error ("Repeated variables on left hand side of function")
             in
               trns
               |> message msg (fn trns => trns
               |> fold_map (exprgen_eq o dest_eqthm) eq_thms
-              |-> (fn eqs => pair (map checkvars eqs))
               ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
               ||>> exprgen_type thy algbr funcgr strct ty
               |-> (fn ((eqs, vs), ty) => succeed (Fun (eqs, (vs, ty)))))
@@ -342,7 +327,7 @@
     val strict = check_strict (CodegenSerializer.const_has_serialization thy) idf strct;
   in
     trns
-    |> debug_msg (fn _ => "generating constant "
+    |> tracing (fn _ => "generating constant "
         ^ (quote o CodegenConsts.string_of_const thy) (c, tys))
     |> ensure_def (get_defgen funcgr strct idf) strict ("generating constant "
          ^ CodegenConsts.string_of_const thy (c, tys)) idf
@@ -415,24 +400,18 @@
         |> appgen_default thy algbr funcgr strct ((f, ty), ts);
 
 
-(* entry points into extraction kernel *)
+(* entrance points into extraction kernel *)
 
 fun ensure_def_const' thy algbr funcgr strct c trns =
   ensure_def_const thy algbr funcgr strct c trns
-  handle CONSTRAIN (((c, ty), ty_decl), NONE) => error (
+  handle CONSTRAIN ((c, ty), ty_decl) => error (
     "Constant " ^ c ^ " with most general type\n"
     ^ Sign.string_of_typ thy ty
     ^ "\noccurs with type\n"
-    ^ Sign.string_of_typ thy ty_decl)
-  handle CONSTRAIN (((c, ty), ty_decl), SOME t) => error ("In term " ^ (quote o Sign.string_of_term thy) t
-    ^ ",\nconstant " ^ c ^ " with most general type\n"
-    ^ Sign.string_of_typ thy ty
-    ^ "\noccurs with type\n"
     ^ Sign.string_of_typ thy ty_decl);
-
 fun exprgen_term' thy algbr funcgr strct t trns =
   exprgen_term thy algbr funcgr strct t trns
-  handle CONSTRAIN (((c, ty), ty_decl), _) => error ("In term " ^ (quote o Sign.string_of_term thy) t
+  handle CONSTRAIN ((c, ty), ty_decl) => error ("In term " ^ (quote o Sign.string_of_term thy) t
     ^ ",\nconstant " ^ c ^ " with most general type\n"
     ^ Sign.string_of_typ thy ty
     ^ "\noccurs with type\n"
@@ -444,16 +423,13 @@
 
 fun appgen_numeral int_of_numeral thy algbr funcgr strct (app as (c, ts)) trns =
   case try (int_of_numeral thy) (list_comb (Const c, ts))
-   of SOME i => (*if i < 0 then (*preprocessor eliminates negative numerals*)
+   of SOME i =>
         trns
-        |> appgen_default thy algbr funcgr (no_strict strct) app
-      else*)
-        trns
-        |> appgen_default thy algbr funcgr (no_strict strct) app
+        |> appgen_default thy algbr funcgr strct app
         |-> (fn e => pair (CodegenThingol.INum (i, e)))
     | NONE =>
         trns
-        |> appgen_default thy algbr funcgr (no_strict strct) app;
+        |> appgen_default thy algbr funcgr strct app;
 
 fun appgen_char char_to_index thy algbr funcgr strct (app as ((_, ty), _)) trns =
   case (char_to_index o list_comb o apfst Const) app
@@ -521,9 +497,18 @@
 
 fun codegen_term thy t =
   let
+    fun const_typ (c, ty) =
+      let
+        val const = CodegenConsts.norm_of_typ thy (c, ty);
+        val funcgr = CodegenFuncgr.mk_funcgr thy [const] [];
+      in case CodegenFuncgr.get_funcs funcgr const
+       of (thm :: _) => CodegenData.typ_func thy thm
+        | [] => Sign.the_const_type thy c
+      end;
     val ct = Thm.cterm_of thy t;
-    val thm = CodegenData.preprocess_cterm thy ct;
-    val t' = (snd o Logic.dest_equals o Drule.plain_prop_of) thm;
+    val (thm, ct') = CodegenData.preprocess_cterm thy
+      (const_typ) ct;
+    val t' = Thm.term_of ct';
     val cs_rhss = CodegenConsts.consts_of thy t';
   in
     (thm, generate thy cs_rhss (SOME []) NONE exprgen_term' t')
@@ -540,18 +525,7 @@
     val _ = Term.fold_atyps (fn _ =>
       error ("Term" ^ Sign.string_of_term thy t ^ "is polymorhpic"))
       (Term.fastype_of t);
-    fun preprocess_term t =
-      let
-        val x = Free (Name.variant (add_term_names (t, [])) "x", fastype_of t);
-        (* fake definition *)
-        val eq = setmp quick_and_dirty true (SkipProof.make_thm thy)
-          (Logic.mk_equals (x, t));
-        fun err () = error "preprocess_term: bad preprocessor"
-      in case map prop_of (CodegenFuncgr.preprocess thy [eq])
-       of [Const ("==", _) $ x' $ t'] => if x = x' then t' else err ()
-        | _ => err ()
-      end;
-    val (_, t') = codegen_term thy (preprocess_term t);
+    val (_, t') = codegen_term thy t;
   in
     CodegenSerializer.eval_term thy (ref_spec, t') (Code.get thy)
   end;
@@ -613,7 +587,7 @@
    "code_class", "code_instance", "code_type", "code_const");
 
 val codeP =
-  OuterSyntax.command codeK "generate and serialize executable code for constants" K.diag (
+  OuterSyntax.improper_command codeK "generate and serialize executable code for constants" K.diag (
     Scan.repeat P.term
     -- Scan.repeat (P.$$$ "(" |--
         P.name :-- (fn target => (CodegenSerializer.parse_serializer target >> SOME) || pair NONE)
diff -r 9a24a9121e58 -r 27d049062b56 src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Mon Oct 02 23:00:50 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML	Mon Oct 02 23:00:51 2006 +0200
@@ -95,8 +95,8 @@
   val start_transact: string option -> (transact -> 'a * transact) -> module -> 'a * module;
   val elim_classes: module -> (iterm list * iterm) list * typscheme -> (iterm list * iterm) list * itype;
 
-  val debug: bool ref;
-  val debug_msg: ('a -> string) -> 'a -> 'a;
+  val trace: bool ref;
+  val tracing: ('a -> string) -> 'a -> 'a;
   val soft_exc: bool ref;
 
   val serialize:
@@ -112,8 +112,8 @@
 
 (** auxiliary **)
 
-val debug = ref false;
-fun debug_msg f x = (if !debug then Output.tracing (f x) else (); x);
+val trace = ref false;
+fun tracing f x = (if !trace then Output.tracing (f x) else (); x);
 val soft_exc = ref true;
 
 fun unfoldl dest x =
@@ -1057,7 +1057,7 @@
       ^ (if strict then " (strict)" else " (non-strict)");
     fun add_dp NONE = I
       | add_dp (SOME dep) =
-          debug_msg (fn _ => "adding dependency " ^ quote dep ^ " -> " ^ quote name)
+          tracing (fn _ => "adding dependency " ^ quote dep ^ " -> " ^ quote name)
           #> add_dep (dep, name);
     fun prep_def def modl =
       (check_prep_def modl def, modl);
@@ -1077,22 +1077,22 @@
     modl
     |> (if can (get_def modl) name
         then
-          debug_msg (fn _ => "asserting node " ^ quote name)
+          tracing (fn _ => "asserting node " ^ quote name)
           #> add_dp dep
         else
-          debug_msg (fn _ => "allocating node " ^ quote name ^ (if strict then " (strict)" else " (non-strict)"))
+          tracing (fn _ => "allocating node " ^ quote name ^ (if strict then " (strict)" else " (non-strict)"))
           #> ensure_bot name
           #> add_dp dep
-          #> debug_msg (fn _ => "creating node " ^ quote name)
+          #> tracing (fn _ => "creating node " ^ quote name)
           #> invoke_generator name defgen
           #-> (fn def => prep_def def)
           #-> (fn def =>
-             debug_msg (fn _ => "addition of " ^ name ^ " := " ^ (Pretty.output o pretty_def) def)
-          #> debug_msg (fn _ => "adding")
+             tracing (fn _ => "addition of " ^ name ^ " := " ^ (Pretty.output o pretty_def) def)
+          #> tracing (fn _ => "adding")
           #> add_def_incr strict (name, def)
-          #> debug_msg (fn _ => "postprocessing")
+          #> tracing (fn _ => "postprocessing")
           #> postprocess_def (name, def)
-          #> debug_msg (fn _ => "adding done")
+          #> tracing (fn _ => "adding done")
        ))
     |> pair dep
   end;