--- a/src/HOL/Tools/inductive_realizer.ML Wed Dec 03 21:00:39 2008 -0800
+++ b/src/HOL/Tools/inductive_realizer.ML Thu Dec 04 14:43:33 2008 +0100
@@ -338,7 +338,7 @@
(Logic.strip_assums_concl rintr));
val s' = Sign.base_name s;
val T' = Logic.unvarifyT T
- in (((Name.binding s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
+ in (((Binding.name s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T))
(List.take (snd (strip_comb
(HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
@@ -347,10 +347,10 @@
val (ind_info, thy3') = thy2 |>
InductivePackage.add_inductive_global (serial_string ())
- {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Name.no_binding,
+ {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty,
coind = false, no_elim = false, no_ind = false, skip_mono = false}
rlzpreds rlzparams (map (fn (rintr, intr) =>
- ((Name.binding (Sign.base_name (name_of_thm intr)), []),
+ ((Binding.name (Sign.base_name (name_of_thm intr)), []),
subst_atomic rlzpreds' (Logic.unvarify rintr)))
(rintrs ~~ maps snd rss)) [] ||>
Sign.absolute_path;