equal
deleted
inserted
replaced
52 |
52 |
53 |
53 |
54 (* variables -- ordered left-to-right, preferring right *) |
54 (* variables -- ordered left-to-right, preferring right *) |
55 |
55 |
56 fun vars_of tm = |
56 fun vars_of tm = |
57 Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm [] |
57 rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm [])); |
58 |> gen_distinct (op =) |
|
59 |> rev; |
|
60 |
58 |
61 local |
59 local |
62 |
60 |
63 val mk_var = encode_type o #2 o Term.dest_Var; |
61 val mk_var = encode_type o #2 o Term.dest_Var; |
64 |
62 |