src/HOL/Subst/Unify.ML

 
 
 (*---------------------------------------------------------------------------
  * The non-nested TC plus the wellfoundedness of unifyRel.
  *---------------------------------------------------------------------------*)
-Tfl.tgoalw Unify.thy [] unify.rules;
+Tfl.tgoalw Unify.thy [] unify.simps;
 (* Wellfoundedness of unifyRel *)
 by (simp_tac (simpset() addsimps [unifyRel_def,
 				 wf_inv_image, wf_lex_prod, wf_finite_psubset,
 				 wf_measure]) 1);
 (* TC *)

  * Eliminate tc0 from the recursion equations and the induction theorem.
  *---------------------------------------------------------------------------*)
 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;
+                     unify.simps;
 
 val unifyInduct0 = [wfr,tc] MRS unify.induct;
 
 
 (*---------------------------------------------------------------------------

 by (Blast_tac 1);
 qed_spec_mp "unify_TC";
 
 
 (*---------------------------------------------------------------------------
- * Now for elimination of nested TC from unify.rules and induction. 
+ * Now for elimination of nested TC from unify.simps and induction. 
  *---------------------------------------------------------------------------*)
 
 (*Desired rule, copied from the theory file.  Could it be made available?*)
 Goal "unify(Comb M1 N1, Comb M2 N2) =      \
 \      (case unify(M1,M2)               \