changeset 16787 | b6b6e2faaa41 |
parent 16424 | 18a07ad8fea8 |
child 17184 | 3d80209e9a53 |
--- a/src/Pure/Isar/induct_attrib.ML Wed Jul 13 10:48:21 2005 +0200 +++ b/src/Pure/Isar/induct_attrib.ML Wed Jul 13 11:16:34 2005 +0200 @@ -56,7 +56,7 @@ local fun rev_vars_of tm = - Term.foldl_aterms (fn (ts, t as Var _) => t :: ts | (ts, _) => ts) ([], tm) + Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm [] |> Library.distinct; val mk_var = encode_type o #2 o Term.dest_Var;