# HG changeset patch
# User paulson
# Date 849181668 -3600
# Node ID d1bcc10be8d7773b7dc2223841cf67da40d3418b
# Parent  d6abc468e40c734032758314225d1c6da4e78868
Fixed spelling error

diff -r d6abc468e40c -r d1bcc10be8d7 src/Provers/nat_transitive.ML
--- a/src/Provers/nat_transitive.ML	Thu Nov 28 12:39:02 1996 +0100
+++ b/src/Provers/nat_transitive.ML	Thu Nov 28 12:47:48 1996 +0100
@@ -11,7 +11,7 @@
 t = u, t < u, t <= u, ~(t < u), ~(t <= u)
 
 where t and u must be of type nat, to
-1. either derive a constradiction,
+1. either derive a contradiction,
    in which case the conclusion can be any term,
 2. or prove the conclusion, which must be of the same form as the premises.
 
@@ -225,7 +225,7 @@
 val trans_tac = SUBGOAL (fn (A,n) =>
   let val Hs = Logic.strip_assums_hyp A
       val C = Logic.strip_assums_concl A
-      val lesss = flat(map mkasm (Hs ~~ (0 upto (length Hs - 1))));
+      val lesss = flat(ListPair.map mkasm (Hs, 0 upto (length Hs - 1)))
       val clesss = close [] lesss
       val (subgoals,prf) = mkconcl C
       val prfs = map (solve clesss) subgoals