src/HOL/Tools/Quotient/quotient_term.ML
changeset 61424 c3658c18b7bc
parent 61125 4c68426800de
child 67632 3b94553353ae
     1.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -634,12 +634,12 @@
     1.4            end
     1.5        end
     1.6  
     1.7 -  | (((t1 as Const (@{const_name uncurry}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
     1.8 -     ((t2 as Const (@{const_name uncurry}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
     1.9 +  | (((t1 as Const (@{const_name case_prod}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
    1.10 +     ((t2 as Const (@{const_name case_prod}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
    1.11         regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
    1.12  
    1.13 -  | (((t1 as Const (@{const_name uncurry}, _)) $ Abs (v1, ty, s1)),
    1.14 -     ((t2 as Const (@{const_name uncurry}, _)) $ Abs (v2, _ , s2))) =>
    1.15 +  | (((t1 as Const (@{const_name case_prod}, _)) $ Abs (v1, ty, s1)),
    1.16 +     ((t2 as Const (@{const_name case_prod}, _)) $ Abs (v2, _ , s2))) =>
    1.17         regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
    1.18  
    1.19    | (t1 $ t2, t1' $ t2') =>