src/HOL/UNITY/Comp.thy
changeset 61424 c3658c18b7bc
parent 59807 22bc39064290
child 61941 31f2105521ee
     1.1 --- a/src/HOL/UNITY/Comp.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/UNITY/Comp.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -186,7 +186,7 @@
     1.4  apply simp
     1.5  apply (subgoal_tac "G \<in> preserves (funPair v w) ")
     1.6   prefer 2 apply simp
     1.7 -apply (drule_tac P1 = "split Q" for Q in preserves_subset_stable [THEN subsetD], 
     1.8 +apply (drule_tac P1 = "case_prod Q" for Q in preserves_subset_stable [THEN subsetD], 
     1.9         auto)
    1.10  done
    1.11