src/HOL/Tools/datatype_realizer.ML
changeset 22691 290454649b8c
parent 22596 d0d2af4db18f
child 23577 c5b93c69afd3
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Sun Apr 15 14:31:44 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Sun Apr 15 14:31:47 2007 +0200
     1.3 @@ -136,7 +136,7 @@
     1.4        ||> Theory.restore_naming thy;
     1.5  
     1.6      val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
     1.7 -    val rvs = rev (Drule.fold_terms Term.add_vars thm' []);
     1.8 +    val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
     1.9      val ivs1 = map Var (filter_out (fn (_, T) =>
    1.10        tname_of (body_type T) mem ["set", "bool"]) ivs);
    1.11      val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (AList.lookup (op =) rvs ixn))) ivs;