--- a/src/HOL/Nominal/nominal_inductive.ML Thu Oct 04 14:42:11 2007 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Thu Oct 04 14:42:47 2007 +0200
@@ -148,7 +148,7 @@
| xs => error ("Missing equivariance theorem for predicate(s): " ^
commas_quote xs));
val induct_cases = map fst (fst (RuleCases.get (the
- (InductAttrib.lookup_inductS ctxt (hd names)))));
+ (Induct.lookup_inductS ctxt (hd names)))));
val raw_induct' = Logic.unvarify (prop_of raw_induct);
val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb);