src/Pure/conjunction.ML
changeset 21565 bd28361f4c5b
parent 20666 82638257d372
child 23422 4a368c087f58
     1.1 --- a/src/Pure/conjunction.ML	Mon Nov 27 23:48:10 2006 +0100
     1.2 +++ b/src/Pure/conjunction.ML	Tue Nov 28 00:35:18 2006 +0100
     1.3 @@ -216,7 +216,7 @@
     1.4      val intro =
     1.5        (eq RS Drule.equal_elim_rule2)
     1.6        |> curry n
     1.7 -      |> K (n = 0) ? Thm.eq_assumption 1;
     1.8 +      |> n = 0 ? Thm.eq_assumption 1;
     1.9      val dests = map (project (eq RS Drule.equal_elim_rule1)) (1 upto n);
    1.10    in (intro, dests) end;
    1.11