src/Pure/raw_simplifier.ML
changeset 60642 48dd1cefb4ae
parent 60324 f83406084507
child 60822 4f58f3662e7d
     1.1 --- a/src/Pure/raw_simplifier.ML	Fri Jul 03 16:19:45 2015 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Sun Jul 05 15:02:30 2015 +0200
     1.3 @@ -1044,8 +1044,9 @@
     1.4              then NONE else SOME thm2'))
     1.5    end;
     1.6  
     1.7 -val (cA, (cB, cC)) =
     1.8 -  apsnd Thm.dest_equals (Thm.dest_implies (hd (cprems_of Drule.imp_cong)));
     1.9 +val vA = (("A", 0), propT);
    1.10 +val vB = (("B", 0), propT);
    1.11 +val vC = (("C", 0), propT);
    1.12  
    1.13  fun transitive1 NONE NONE = NONE
    1.14    | transitive1 (SOME thm1) NONE = SOME thm1
    1.15 @@ -1177,7 +1178,7 @@
    1.16          val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
    1.17          val eq' =
    1.18            Thm.implies_elim
    1.19 -            (Thm.instantiate ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong)
    1.20 +            (Thm.instantiate ([], [(vA, prem), (vB, lhs), (vC, rhs)]) Drule.imp_cong)
    1.21              (Thm.implies_intr prem eq);
    1.22        in
    1.23          if not r then eq'
    1.24 @@ -1188,9 +1189,9 @@
    1.25            in
    1.26              Thm.transitive
    1.27                (Thm.transitive
    1.28 -                (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)]) Drule.swap_prems_eq)
    1.29 +                (Thm.instantiate ([], [(vA, prem'), (vB, prem), (vC, concl)]) Drule.swap_prems_eq)
    1.30                  eq')
    1.31 -              (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)]) Drule.swap_prems_eq)
    1.32 +              (Thm.instantiate ([], [(vA, prem), (vB, prem''), (vC, concl)]) Drule.swap_prems_eq)
    1.33            end
    1.34        end
    1.35