tmp fix to accomodate rep_ss changes;
authorwenzelm
Wed Jul 23 10:34:18 1997 +0200 (1997-07-23)
changeset 3556229a40c2b19e
parent 3555 5a720f6b9f38
child 3557 9546f8185c43
tmp fix to accomodate rep_ss changes;
TFL/post.sml
TFL/rules.new.sml
     1.1 --- a/TFL/post.sml	Wed Jul 23 10:22:48 1997 +0200
     1.2 +++ b/TFL/post.sml	Wed Jul 23 10:34:18 1997 +0200
     1.3 @@ -154,7 +154,8 @@
     1.4                       if (solved th) then (th::So, Si, St) 
     1.5                       else (So, th::Si, St)) nested_tcs ([],[],[])
     1.6                val simplified' = map join_assums simplified
     1.7 -              val rewr = rewrite (solved @ simplified' @ #simps(rep_ss ss))
     1.8 +              val rewr = rewrite (solved @ simplified' @
     1.9 +                #simps (Thm.dest_mss (#mss (rep_ss ss))));
    1.10                val induction' = rewr induction
    1.11                and rules'     = rewr rules
    1.12                val dummy = writeln "Postprocessing done."
     2.1 --- a/TFL/rules.new.sml	Wed Jul 23 10:22:48 1997 +0200
     2.2 +++ b/TFL/rules.new.sml	Wed Jul 23 10:34:18 1997 +0200
     2.3 @@ -393,7 +393,7 @@
     2.4  local fun rew_conv mss = rewrite_cterm (true,false) mss (K(K None))
     2.5  in
     2.6  fun simpl_conv ss thl ctm = 
     2.7 - rew_conv (Thm.mss_of (#simps(rep_ss ss)@thl)) ctm
     2.8 + rew_conv (Thm.mss_of (#simps (Thm.dest_mss (#mss (rep_ss ss))) @ thl)) ctm
     2.9   RS meta_eq_to_obj_eq
    2.10  end;
    2.11