--- a/src/HOL/Tools/datatype_realizer.ML Sun Apr 15 14:31:44 2007 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Sun Apr 15 14:31:47 2007 +0200
@@ -136,7 +136,7 @@
||> Theory.restore_naming thy;
val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
- val rvs = rev (Drule.fold_terms Term.add_vars thm' []);
+ val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
val ivs1 = map Var (filter_out (fn (_, T) =>
tname_of (body_type T) mem ["set", "bool"]) ivs);
val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (AList.lookup (op =) rvs ixn))) ivs;