Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tmp fix to accomodate rep_ss changes;
authorwenzelm
Wed, 23 Jul 1997 10:34:18 +0200
changeset 3556 229a40c2b19e
parent 3555 5a720f6b9f38
child 3557 9546f8185c43
tmp fix to accomodate rep_ss changes;
TFL/post.sml file | annotate | diff | comparison | revisions
TFL/rules.new.sml file | annotate | diff | comparison | revisions 
--- 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."
--- a/TFL/rules.new.sml	Wed Jul 23 10:22:48 1997 +0200
+++ b/TFL/rules.new.sml	Wed Jul 23 10:34:18 1997 +0200
@@ -393,7 +393,7 @@
 local fun rew_conv mss = rewrite_cterm (true,false) mss (K(K None))
 in
 fun simpl_conv ss thl ctm = 
- rew_conv (Thm.mss_of (#simps(rep_ss ss)@thl)) ctm
+ rew_conv (Thm.mss_of (#simps (Thm.dest_mss (#mss (rep_ss ss))) @ thl)) ctm
  RS meta_eq_to_obj_eq
 end;
isabelle