src/Pure/conjunction.ML

--- a/src/Pure/conjunction.ML	Mon Nov 27 23:48:10 2006 +0100
+++ b/src/Pure/conjunction.ML	Tue Nov 28 00:35:18 2006 +0100
@@ -216,7 +216,7 @@
     val intro =
       (eq RS Drule.equal_elim_rule2)
       |> curry n
-      |> K (n = 0) ? Thm.eq_assumption 1;
+      |> n = 0 ? Thm.eq_assumption 1;
     val dests = map (project (eq RS Drule.equal_elim_rule1)) (1 upto n);
   in (intro, dests) end;