changeset 19046 | bc5c6c9b114e |
parent 18977 | f24c416a4814 |
child 21506 | b2a673894ce5 |
--- a/src/Pure/Isar/induct_attrib.ML Wed Feb 15 19:11:10 2006 +0100 +++ b/src/Pure/Isar/induct_attrib.ML Wed Feb 15 21:34:55 2006 +0100 @@ -54,9 +54,7 @@ (* variables -- ordered left-to-right, preferring right *) fun vars_of tm = - Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm [] - |> gen_distinct (op =) - |> rev; + rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm [])); local