diff -r 5e45dd3b64e9 -r d0d86b96aa96 src/HOL/Subst/Unify.ML
--- a/src/HOL/Subst/Unify.ML	Tue Jun 03 11:08:08 1997 +0200
+++ b/src/HOL/Subst/Unify.ML	Tue Jun 03 12:03:38 1997 +0200
@@ -127,7 +127,8 @@
 (*---------------------------------------------------------------------------
  * Eliminate tc0 from the recursion equations and the induction theorem.
  *---------------------------------------------------------------------------*)
-val [wfr,tc] = Prim.Rules.CONJUNCTS tc0;
+val wfr = tc0 RS conjunct1
+and tc  = tc0 RS conjunct2;
 val unifyRules0 = map (normalize_thm [fn th => wfr RS th, fn th => tc RS th]) 
                      unify.rules;