--- a/src/HOL/Tools/inductive_package.ML Mon Dec 01 16:02:57 2008 +0100
+++ b/src/HOL/Tools/inductive_package.ML Mon Dec 01 19:41:16 2008 +0100
@@ -638,8 +638,8 @@
(* add definiton of recursive predicates to theory *)
val rec_name =
- if Name.is_nothing alt_name then
- Name.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
+ if Binding.is_nothing alt_name then
+ Binding.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
else alt_name;
val ((rec_const, (_, fp_def)), ctxt') = ctxt |>