TFL/post.sml

                U.itlist (fn th => fn (So,Si,St) =>
                      if (id_thm th) then (So, Si, th::St) else
                      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(rep_ss ss))
+              val rewr = rewrite (solved @ simplified' @
+                #simps (Thm.dest_mss (#mss (rep_ss ss))));
               val induction' = rewr induction
               and rules'     = rewr rules
               val dummy = writeln "Postprocessing done."
           in
           {induction = induction',