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;