# HG changeset patch
# User wenzelm
# Date 968353177 -7200
# Node ID 09253f667beb3679f341066374aa9440ef91f02e
# Parent  d087c8dae285a43e595625ec1a30381af736c8a9
use Rulify.rulify_no_asm;

diff -r d087c8dae285 -r 09253f667beb TFL/post.sml
--- a/TFL/post.sml	Thu Sep 07 20:58:54 2000 +0200
+++ b/TFL/post.sml	Thu Sep 07 20:59:37 2000 +0200
@@ -176,8 +176,8 @@
                {f = f, R = R, rules = rules,
                 full_pats_TCs = full_pats_TCs,
                 TCs = TCs}
-       val rules' = map (standard o rulify) (R.CONJUNCTS rules)
-   in  {induct = meta_outer (rulify (induction RS spec')),
+       val rules' = map (standard o Rulify.rulify_no_asm) (R.CONJUNCTS rules)
+   in  {induct = meta_outer (Rulify.rulify_no_asm (induction RS spec')),
         rules = ListPair.zip(rules', rows),
         tcs = (termination_goals rules') @ tcs}
    end