No longer refers to internal TFL structures
authorpaulson
Tue Jun 03 12:03:38 1997 +0200 (1997-06-03)
changeset 3392d0d86b96aa96
parent 3391 5e45dd3b64e9
child 3393 e31ac367387e
No longer refers to internal TFL structures
src/HOL/Subst/Unify.ML
     1.1 --- a/src/HOL/Subst/Unify.ML	Tue Jun 03 11:08:08 1997 +0200
     1.2 +++ b/src/HOL/Subst/Unify.ML	Tue Jun 03 12:03:38 1997 +0200
     1.3 @@ -127,7 +127,8 @@
     1.4  (*---------------------------------------------------------------------------
     1.5   * Eliminate tc0 from the recursion equations and the induction theorem.
     1.6   *---------------------------------------------------------------------------*)
     1.7 -val [wfr,tc] = Prim.Rules.CONJUNCTS tc0;
     1.8 +val wfr = tc0 RS conjunct1
     1.9 +and tc  = tc0 RS conjunct2;
    1.10  val unifyRules0 = map (normalize_thm [fn th => wfr RS th, fn th => tc RS th]) 
    1.11                       unify.rules;
    1.12