equal
deleted
inserted
replaced
128 fun translate (t, cs) = |
128 fun translate (t, cs) = |
129 let val T = Term.fastype_of t |
129 let val T = Term.fastype_of t |
130 in |
130 in |
131 (case (can HOLogic.dest_number t, cs) of |
131 (case (can HOLogic.dest_number t, cs) of |
132 (true, [c]) => trans 0 T c #>> (fn (_, u) => [mk_eq u ([], t)]) |
132 (true, [c]) => trans 0 T c #>> (fn (_, u) => [mk_eq u ([], t)]) |
133 | (_, (es, _) :: _) => fold_map (trans (length es) T) cs #>> map (mk_eq t)) |
133 | (_, (es, _) :: _) => fold_map (trans (length es) T) cs #>> map (mk_eq t) |
|
134 | _ => raise TERM ("translate: no cases", [t])) |
134 end |
135 end |
135 |
136 |
136 |
137 |
137 (* overall procedure *) |
138 (* overall procedure *) |
138 |
139 |