diff -r f1c8fa0f0bf9 -r 5ec1589eac1b TFL/post.sml
--- a/TFL/post.sml	Thu Jul 24 11:12:18 1997 +0200
+++ b/TFL/post.sml	Thu Jul 24 11:13:12 1997 +0200
@@ -154,8 +154,7 @@
                      if (solved th) then (th::So, Si, St) 
                      else (So, th::Si, St)) nested_tcs ([],[],[])
               val simplified' = map join_assums simplified
-              val rewr = rewrite (solved @ simplified' @
-                #simps (Thm.dest_mss (#mss (rep_ss ss))));
+              val rewr = full_simplify (ss addsimps (solved @ simplified'));
               val induction' = rewr induction
               and rules'     = rewr rules
               val dummy = writeln "Postprocessing done."