# HG changeset patch
# User paulson
# Date 958137535 -7200
# Node ID 851693e780d65afd10c3aeae232fce6f7dc96b86
# Parent  06dcd62f65ad266ad191a31ae94f47fb141b04a6
nat_diff_split' now called nat_diff_split

diff -r 06dcd62f65ad -r 851693e780d6 src/HOL/UNITY/Token.ML
--- a/src/HOL/UNITY/Token.ML	Fri May 12 15:15:27 2000 +0200
+++ b/src/HOL/UNITY/Token.ML	Fri May 12 15:18:55 2000 +0200
@@ -52,7 +52,7 @@
     "[| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)";
 by (auto_tac (claset(), simpset() addsimps [mod_Suc, mod_geq]));
 by (auto_tac (claset(), 
-              simpset() addsplits [nat_diff_split']
+              simpset() addsplits [nat_diff_split]
                         addsimps [linorder_neq_iff, mod_geq]));
 qed "nodeOrder_eq";