# HG changeset patch # User wenzelm # Date 1003857253 -7200 # Node ID 938dd8bca66184c12c1bed123b663d95836fe4dc # Parent db207d68392c8fa9dd1651d2740c4c79842bc4b5 replace_dummy_patterns: lift over bounds; diff -r db207d68392c -r 938dd8bca661 src/Pure/term.ML --- a/src/Pure/term.ML Tue Oct 23 19:13:44 2001 +0200 +++ b/src/Pure/term.ML Tue Oct 23 19:14:13 2001 +0200 @@ -1076,8 +1076,17 @@ if not (foldl_aterms (fn (b, t) => b orelse is_dummy_pattern t) (false, tm)) then tm else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]); -val replace_dummy_patterns = foldl_map_aterms (fn (i, t) => - if is_dummy_pattern t then (i + 1, Var (("_dummy_", i), fastype_of t)) else (i, t)); +fun replace_dummy Ts (i, Const ("dummy_pattern", T)) = + (i + 1, list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1))) + | replace_dummy Ts (i, Abs (x, T, t)) = + let val (i', t') = replace_dummy (T :: Ts) (i, t) + in (i', Abs (x, T, t')) end + | replace_dummy Ts (i, t $ u) = + let val (i', t') = replace_dummy Ts (i, t); val (i'', u') = replace_dummy Ts (i', u) + in (i'', t' $ u') end + | replace_dummy _ (i, a) = (i, a); + +val replace_dummy_patterns = replace_dummy []; fun is_replaced_dummy_pattern ("_dummy_", _) = true | is_replaced_dummy_pattern _ = false;