src/HOL/Tools/datatype_realizer.ML
changeset 20286 4cf8e86a2d29
parent 20071 8f3e1ddb50e6
child 21646 c07b5b0e8492
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Wed Aug 02 18:33:46 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Wed Aug 02 22:26:37 2006 +0200
     1.3 @@ -136,9 +136,8 @@
     1.4          ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), [])
     1.5        ||> Theory.restore_naming thy;
     1.6  
     1.7 -    val ivs = Drule.vars_of_terms
     1.8 -      [Logic.varify (DatatypeProp.make_ind [descr] sorts)];
     1.9 -    val rvs = Drule.vars_of_terms [prop_of thm'];
    1.10 +    val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
    1.11 +    val rvs = rev (Drule.fold_terms Term.add_vars thm' []);
    1.12      val ivs1 = map Var (filter_out (fn (_, T) =>
    1.13        tname_of (body_type T) mem ["set", "bool"]) ivs);
    1.14      val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (AList.lookup (op =) rvs ixn))) ivs;