src/HOL/Product_Type.thy
changeset 42247 12fe41a92cd5
parent 42083 e1209fc7ecdc
child 42284 326f57825e1a
     1.1 --- a/src/HOL/Product_Type.thy	Wed Apr 06 13:27:59 2011 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Apr 06 13:33:46 2011 +0200
     1.3 @@ -232,8 +232,8 @@
     1.4  (* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *) 
     1.5  typed_print_translation {*
     1.6  let
     1.7 -  fun split_guess_names_tr' _ T [Abs (x, _, Abs _)] = raise Match
     1.8 -    | split_guess_names_tr' _ T [Abs (x, xT, t)] =
     1.9 +  fun split_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
    1.10 +    | split_guess_names_tr' T [Abs (x, xT, t)] =
    1.11          (case (head_of t) of
    1.12            Const (@{const_syntax prod_case}, _) => raise Match
    1.13          | _ =>
    1.14 @@ -245,7 +245,7 @@
    1.15              Syntax.const @{syntax_const "_abs"} $
    1.16                (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
    1.17            end)
    1.18 -    | split_guess_names_tr' _ T [t] =
    1.19 +    | split_guess_names_tr' T [t] =
    1.20          (case head_of t of
    1.21            Const (@{const_syntax prod_case}, _) => raise Match
    1.22          | _ =>
    1.23 @@ -257,7 +257,7 @@
    1.24              Syntax.const @{syntax_const "_abs"} $
    1.25                (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
    1.26            end)
    1.27 -    | split_guess_names_tr' _ _ _ = raise Match;
    1.28 +    | split_guess_names_tr' _ _ = raise Match;
    1.29  in [(@{const_syntax prod_case}, split_guess_names_tr')] end
    1.30  *}
    1.31