src/Pure/term.ML
 changeset 11903 938dd8bca661 parent 11353 7f6eff7bc97a child 11922 78857e6107cb
```     1.1 --- a/src/Pure/term.ML	Tue Oct 23 19:13:44 2001 +0200
1.2 +++ b/src/Pure/term.ML	Tue Oct 23 19:14:13 2001 +0200
1.3 @@ -1076,8 +1076,17 @@
1.4    if not (foldl_aterms (fn (b, t) => b orelse is_dummy_pattern t) (false, tm)) then tm
1.5    else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
1.6
1.7 -val replace_dummy_patterns = foldl_map_aterms (fn (i, t) =>
1.8 -  if is_dummy_pattern t then (i + 1, Var (("_dummy_", i), fastype_of t)) else (i, t));
1.9 +fun replace_dummy Ts (i, Const ("dummy_pattern", T)) =
1.10 +      (i + 1, list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)))
1.11 +  | replace_dummy Ts (i, Abs (x, T, t)) =
1.12 +      let val (i', t') = replace_dummy (T :: Ts) (i, t)
1.13 +      in (i', Abs (x, T, t')) end
1.14 +  | replace_dummy Ts (i, t \$ u) =
1.15 +      let val (i', t') = replace_dummy Ts (i, t); val (i'', u') = replace_dummy Ts (i', u)
1.16 +      in (i'', t' \$ u') end
1.17 +  | replace_dummy _ (i, a) = (i, a);
1.18 +
1.19 +val replace_dummy_patterns = replace_dummy [];
1.20
1.21  fun is_replaced_dummy_pattern ("_dummy_", _) = true
1.22    | is_replaced_dummy_pattern _ = false;
```