Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
TFL/post.sml
changeset 3556 229a40c2b19e
parent 3497 122e80826c95
child 3572 5ec1589eac1b 
--- a/TFL/post.sml	Wed Jul 23 10:22:48 1997 +0200
+++ b/TFL/post.sml	Wed Jul 23 10:34:18 1997 +0200
@@ -154,7 +154,8 @@
                      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."
isabelle