src/HOL/MicroJava/J/Example.thy
changeset 61424 c3658c18b7bc
parent 61361 8b5f00202e1a
child 62042 6c6ccf573479
     1.1 --- a/src/HOL/MicroJava/J/Example.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/MicroJava/J/Example.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -434,7 +434,7 @@
     1.4  apply     (simp (no_asm))
     1.5  apply     (rule e) -- "XcptE"
     1.6  apply    (simp (no_asm))
     1.7 -apply   (rule surjective_pairing [symmetric, THEN[2]trans], subst Pair_eq, force)
     1.8 +apply   (rule surjective_pairing [symmetric, THEN[2]trans], subst prod.inject, force)
     1.9  apply  (simp (no_asm))
    1.10  apply (simp (no_asm))
    1.11  apply (rule e) -- "XcptE"