Reorganized simplifier. May now reorient rules.
authornipkow
Wed Mar 04 13:16:05 1998 +0100 (1998-03-04)
changeset 467924917efb31b5
parent 4678 78715f589655
child 4680 c9d352428201
Reorganized simplifier. May now reorient rules.
Moved loop tests from logic to thm.
src/Pure/drule.ML
src/Pure/logic.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/drule.ML	Wed Mar 04 13:15:05 1998 +0100
     1.2 +++ b/src/Pure/drule.ML	Wed Mar 04 13:16:05 1998 +0100
     1.3 @@ -51,6 +51,7 @@
     1.4    val symmetric_thm	: thm
     1.5    val transitive_thm	: thm
     1.6    val refl_implies      : thm
     1.7 +  val symmetric_fun     : thm -> thm
     1.8    val rewrite_rule_aux	: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
     1.9    val rewrite_thm	: bool * bool -> (meta_simpset -> thm -> thm option)
    1.10  	-> meta_simpset -> thm -> thm
    1.11 @@ -421,6 +422,8 @@
    1.12    in store_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm))
    1.13    end;
    1.14  
    1.15 +fun symmetric_fun thm = thm RS symmetric_thm;
    1.16 +
    1.17  (** Below, a "conversion" has type cterm -> thm **)
    1.18  
    1.19  val refl_implies = reflexive (cterm_of proto_sign implies);
     2.1 --- a/src/Pure/logic.ML	Wed Mar 04 13:15:05 1998 +0100
     2.2 +++ b/src/Pure/logic.ML	Wed Mar 04 13:16:05 1998 +0100
     2.3 @@ -26,9 +26,6 @@
     2.4    val list_flexpairs	: (term*term)list * term -> term
     2.5    val list_implies	: term list * term -> term
     2.6    val list_rename_params: string list * term -> term
     2.7 -  val rewrite_rule_extra_vars: term list -> term -> term -> string option
     2.8 -  val rewrite_rule_ok   : Sign.sg -> term list -> term -> term
     2.9 -                          -> string option * bool
    2.10    val mk_equals		: term * term -> term
    2.11    val mk_flexpair	: term * term -> term
    2.12    val mk_implies	: term * term -> term
    2.13 @@ -304,59 +301,4 @@
    2.14    | unvarify (f$t) = unvarify f $ unvarify t
    2.15    | unvarify t = t;
    2.16  
    2.17 -
    2.18 -
    2.19 -(** Test wellformedness of rewrite rules **)
    2.20 -
    2.21 -fun vperm (Var _, Var _) = true
    2.22 -  | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
    2.23 -  | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
    2.24 -  | vperm (t, u) = (t = u);
    2.25 -
    2.26 -fun var_perm (t, u) =
    2.27 -  vperm (t, u) andalso eq_set_term (term_vars t, term_vars u);
    2.28 -
    2.29 -(*simple test for looping rewrite*)
    2.30 -fun looptest sign prems lhs rhs =
    2.31 -   is_Var (head_of lhs)
    2.32 -  orelse
    2.33 -   (exists (apl (lhs, op occs)) (rhs :: prems))
    2.34 -  orelse
    2.35 -   (null prems andalso
    2.36 -    Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
    2.37 -(*  orelse
    2.38 -   (case lhs of
    2.39 -      (f as Free _) $ (Var _) => exists (fn p => f occs p) prems orelse
    2.40 -                                 (null prems andalso f occs rhs)
    2.41 -    | _ => false)*);
    2.42 -(*the condition "null prems" in the last cases is necessary because
    2.43 -  conditional rewrites with extra variables in the conditions may terminate
    2.44 -  although the rhs is an instance of the lhs. Example:
    2.45 -  ?m < ?n ==> f(?n) == f(?m)*)
    2.46 -(*FIXME: proper test: lhs does not match a subterm of a premise
    2.47 -                      and does not match a subterm of the rhs if null prems *)
    2.48 -
    2.49 -fun rewrite_rule_extra_vars prems elhs erhs =
    2.50 -  if not ((term_vars erhs) subset
    2.51 -          (union_term (term_vars elhs, List.concat(map term_vars prems))))
    2.52 -  then Some("extra Var(s) on rhs") else
    2.53 -  if not ((term_tvars erhs) subset
    2.54 -          (term_tvars elhs  union  List.concat(map term_tvars prems)))
    2.55 -  then Some("extra TVar(s) on rhs")
    2.56 -  else None;
    2.57 -
    2.58 -fun rewrite_rule_ok sign prems lhs rhs =
    2.59 -  let
    2.60 -    val elhs = Pattern.eta_contract lhs;
    2.61 -    val erhs = Pattern.eta_contract rhs;
    2.62 -    val perm = var_perm (elhs, erhs) andalso not (elhs aconv erhs)
    2.63 -               andalso not (is_Var elhs)
    2.64 -  in (case rewrite_rule_extra_vars prems elhs erhs of
    2.65 -        None => if not perm andalso looptest sign prems elhs erhs
    2.66 -                then Some("loops")
    2.67 -                else None
    2.68 -      | some => some
    2.69 -      ,perm)
    2.70 -  end;
    2.71 -
    2.72  end;
     3.1 --- a/src/Pure/thm.ML	Wed Mar 04 13:15:05 1998 +0100
     3.2 +++ b/src/Pure/thm.ML	Wed Mar 04 13:16:05 1998 +0100
     3.3 @@ -164,7 +164,8 @@
     3.4    val add_prems         : meta_simpset * thm list -> meta_simpset
     3.5    val prems_of_mss      : meta_simpset -> thm list
     3.6    val set_mk_rews       : meta_simpset * (thm -> thm list) -> meta_simpset
     3.7 -(*  val mk_rews_of_mss    : meta_simpset -> thm -> thm list *)
     3.8 +  val set_mk_sym        : meta_simpset * (thm -> thm option) -> meta_simpset
     3.9 +  val set_mk_eq_True    : meta_simpset * (thm -> thm option) -> meta_simpset
    3.10    val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
    3.11    val trace_simp        : bool ref
    3.12    val rewrite_cterm     : bool * bool -> meta_simpset ->
    3.13 @@ -1459,6 +1460,9 @@
    3.14  fun prtm warn a sign t =
    3.15    (prnt warn a; prnt warn (Sign.string_of_term sign t));
    3.16  
    3.17 +fun prthm warn a (thm as Thm{sign_ref, prop, ...}) =
    3.18 +  (prtm warn a (Sign.deref sign_ref) prop);
    3.19 +
    3.20  val trace_simp = ref false;
    3.21  
    3.22  fun trace warn a = if !trace_simp then prnt warn a else ();
    3.23 @@ -1505,7 +1509,9 @@
    3.24      bounds: names of bound variables already used
    3.25        (for generating new names when rewriting under lambda abstractions);
    3.26      prems: current premises;
    3.27 -    mk_rews: turns simplification thms into rewrite rules;
    3.28 +    mk_rews: mk: turns simplification thms into rewrite rules;
    3.29 +             mk_sym: turns == around; (needs Drule!)
    3.30 +             mk_eq_True: turns P into P == True - logic specific;
    3.31      termless: relation for ordered rewriting;
    3.32  *)
    3.33  
    3.34 @@ -1516,15 +1522,21 @@
    3.35      procs: simproc Net.net,
    3.36      bounds: string list,
    3.37      prems: thm list,
    3.38 -    mk_rews: thm -> thm list,
    3.39 +    mk_rews: {mk: thm -> thm list,
    3.40 +              mk_sym: thm -> thm option,
    3.41 +              mk_eq_True: thm -> thm option},
    3.42      termless: term * term -> bool};
    3.43  
    3.44  fun mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless) =
    3.45    Mss {rules = rules, congs = congs, procs = procs, bounds = bounds,
    3.46 -    prems = prems, mk_rews = mk_rews, termless = termless};
    3.47 +       prems=prems, mk_rews=mk_rews, termless=termless};
    3.48 +
    3.49 +fun upd_rules(Mss{rules,congs,procs,bounds,prems,mk_rews,termless}, rules') =
    3.50 +  mk_mss(rules',congs,procs,bounds,prems,mk_rews,termless);
    3.51  
    3.52  val empty_mss =
    3.53 -  mk_mss (Net.empty, [], Net.empty, [], [], K [], Term.termless);
    3.54 +  let val mk_rews = {mk = K [], mk_sym = K None, mk_eq_True = K None}
    3.55 +  in mk_mss (Net.empty, [], Net.empty, [], [], mk_rews, Term.termless) end;
    3.56  
    3.57  
    3.58  
    3.59 @@ -1556,65 +1568,123 @@
    3.60          generic_merge eq_prem I I prems1 prems2,
    3.61          mk_rews, termless);
    3.62  
    3.63 +(* add_simps *)
    3.64  
    3.65 -(* mk_rrule *)
    3.66 +fun insert_rrule(mss as Mss {rules,...},
    3.67 +                 rrule as {thm = thm, lhs = lhs, perm = perm}) =
    3.68 +  (trace_thm false "Adding rewrite rule:" thm;
    3.69 +   let val rules' = Net.insert_term ((lhs, rrule), rules, eq_rrule)
    3.70 +   in upd_rules(mss,rules') end
    3.71 +   handle Net.INSERT =>
    3.72 +     (prthm true "Ignoring duplicate rewrite rule" thm; mss));
    3.73 +
    3.74 +fun vperm (Var _, Var _) = true
    3.75 +  | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
    3.76 +  | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
    3.77 +  | vperm (t, u) = (t = u);
    3.78 +
    3.79 +fun var_perm (t, u) =
    3.80 +  vperm (t, u) andalso eq_set_term (term_vars t, term_vars u);
    3.81 +
    3.82 +(* FIXME: it seems that the conditions on extra variables are too liberal if
    3.83 +prems are nonempty: does solving the prems really guarantee instantiation of
    3.84 +all its Vars? Better: a dynamic check each time a rule is applied.
    3.85 +*)
    3.86 +fun rewrite_rule_extra_vars prems elhs erhs =
    3.87 +  not ((term_vars erhs) subset
    3.88 +       (union_term (term_vars elhs, List.concat(map term_vars prems))))
    3.89 +  orelse
    3.90 +  not ((term_tvars erhs) subset
    3.91 +       (term_tvars elhs  union  List.concat(map term_tvars prems)));
    3.92  
    3.93 -fun mk_rrule (thm as Thm {sign_ref, prop, ...}) =
    3.94 -  let
    3.95 -    val sign = Sign.deref sign_ref;
    3.96 -    val prems = Logic.strip_imp_prems prop;
    3.97 -    val concl = Logic.strip_imp_concl prop;
    3.98 -    val (lhs, rhs) = Logic.dest_equals concl handle TERM _ =>
    3.99 -      raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
   3.100 -  in case Logic.rewrite_rule_ok sign prems lhs rhs of
   3.101 -     (None,perm) => Some {thm = thm, lhs = lhs, perm = perm}
   3.102 -   | (Some msg,_) =>
   3.103 -        (prtm true ("ignoring rewrite rule ("^msg^")") sign prop; None)
   3.104 +(*simple test for looping rewrite*)
   3.105 +fun looptest sign prems lhs rhs =
   3.106 +   rewrite_rule_extra_vars prems lhs rhs
   3.107 +  orelse
   3.108 +   is_Var (head_of lhs)
   3.109 +  orelse
   3.110 +   (exists (apl (lhs, op Logic.occs)) (rhs :: prems))
   3.111 +  orelse
   3.112 +   (null prems andalso
   3.113 +    Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
   3.114 +(*the condition "null prems" in the last cases is necessary because
   3.115 +  conditional rewrites with extra variables in the conditions may terminate
   3.116 +  although the rhs is an instance of the lhs. Example:
   3.117 +  ?m < ?n ==> f(?n) == f(?m)*)
   3.118 +
   3.119 +fun decomp_simp(thm as Thm {sign_ref, prop, ...}) =
   3.120 +  let val sign = Sign.deref sign_ref;
   3.121 +      val prems = Logic.strip_imp_prems prop;
   3.122 +      val concl = Logic.strip_imp_concl prop;
   3.123 +      val (lhs, rhs) = Logic.dest_equals concl handle TERM _ =>
   3.124 +        raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm)
   3.125 +      val elhs = Pattern.eta_contract lhs;
   3.126 +      val erhs = Pattern.eta_contract rhs;
   3.127 +      val perm = var_perm (elhs, erhs) andalso not (elhs aconv erhs)
   3.128 +                 andalso not (is_Var elhs)
   3.129 +  in (sign,prems,lhs,rhs,perm) end;
   3.130 +
   3.131 +fun mk_eq_True (Mss{mk_rews={mk_eq_True,...},...}) thm =
   3.132 +  apsome (fn eq_True => let val (_,_,lhs,_,_) = decomp_simp eq_True
   3.133 +                        in {thm=eq_True, lhs=lhs, perm=false} end)
   3.134 +         (mk_eq_True thm);
   3.135 +
   3.136 +fun mk_rrule mss thm =
   3.137 +  let val (_,prems,lhs,rhs,perm) = decomp_simp thm
   3.138 +  in if perm then Some{thm=thm, lhs=lhs, perm=true} else
   3.139 +     (* weak test for loops: *)
   3.140 +     if rewrite_rule_extra_vars prems lhs rhs orelse
   3.141 +        is_Var (head_of lhs) (* mk_cases may do this! *)
   3.142 +     then mk_eq_True mss thm
   3.143 +     else Some{thm=thm, lhs=lhs, perm=false}
   3.144    end;
   3.145  
   3.146 +fun orient_rrule mss thm =
   3.147 +  let val (sign,prems,lhs,rhs,perm) = decomp_simp thm
   3.148 +  in if perm then Some{thm=thm,lhs=lhs,perm=true}
   3.149 +     else if looptest sign prems lhs rhs
   3.150 +          then if looptest sign prems rhs lhs
   3.151 +               then mk_eq_True mss thm
   3.152 +               else let val Mss{mk_rews={mk_sym,...},...} = mss
   3.153 +                    in apsome (fn thm' => {thm=thm', lhs=rhs, perm=false})
   3.154 +                              (mk_sym thm)
   3.155 +                    end
   3.156 +          else Some{thm=thm, lhs=lhs, perm=false}
   3.157 +  end;
   3.158  
   3.159 -(* add_simps *)
   3.160 +fun extract_rews(Mss{mk_rews = {mk,...},...},thms) = flat(map mk thms);
   3.161  
   3.162 -fun add_simp1(mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless},
   3.163 -              thm as Thm {sign_ref, prop, ...}) =
   3.164 -  case mk_rrule thm of
   3.165 -    None => mss
   3.166 -  | Some (rrule as {lhs, ...}) =>
   3.167 -      (trace_thm false "Adding rewrite rule:" thm;
   3.168 -       mk_mss (Net.insert_term ((lhs, rrule), rules, eq_rrule),
   3.169 -               congs, procs, bounds, prems, mk_rews, termless)
   3.170 -       handle Net.INSERT =>
   3.171 -       (prtm true "ignoring duplicate rewrite rule" (Sign.deref sign_ref) prop;
   3.172 -        mss));
   3.173 +fun orient_comb_simps comb mk_rrule (mss,thms) =
   3.174 +  let val rews = extract_rews(mss,thms)
   3.175 +      val rrules = mapfilter mk_rrule rews
   3.176 +  in foldl comb (mss,rrules) end
   3.177  
   3.178 -fun add_simp(mss as Mss{mk_rews,...},thm) = foldl add_simp1 (mss, mk_rews thm);
   3.179 +(* Add rewrite rules explicitly; do not reorient! *)
   3.180 +fun add_simps(mss,thms) =
   3.181 +  orient_comb_simps insert_rrule (mk_rrule mss) (mss,thms);
   3.182  
   3.183 -val add_simps = foldl add_simp;
   3.184 +fun mss_of thms =
   3.185 +  foldl insert_rrule (empty_mss, mapfilter (mk_rrule empty_mss) thms);
   3.186  
   3.187 -fun mss_of thms = foldl add_simp1 (empty_mss, thms);
   3.188 +fun safe_add_simps(mss,thms) =
   3.189 +  orient_comb_simps insert_rrule (orient_rrule mss) (mss,thms);
   3.190  
   3.191  
   3.192  (* del_simps *)
   3.193  
   3.194 -fun del_simp1(mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless},
   3.195 -              thm as Thm {sign_ref, prop, ...}) =
   3.196 -  case mk_rrule thm of
   3.197 -    None => mss
   3.198 -  | Some (rrule as {lhs, ...}) =>
   3.199 -      (mk_mss (Net.delete_term ((lhs, rrule), rules, eq_rrule),
   3.200 -               congs, procs, bounds, prems, mk_rews, termless)
   3.201 -       handle Net.DELETE =>
   3.202 -       (prtm true "rewrite rule not in simpset" (Sign.deref sign_ref) prop;
   3.203 -        mss));
   3.204 +fun del_rrule(mss as Mss {rules,...},
   3.205 +              rrule as {thm = thm, lhs = lhs, perm = perm}) =
   3.206 +  (upd_rules(mss, Net.delete_term ((lhs, rrule), rules, eq_rrule))
   3.207 +   handle Net.DELETE =>
   3.208 +     (prthm true "rewrite rule not in simpset" thm; mss));
   3.209  
   3.210 -fun del_simp(mss as Mss{mk_rews,...},thm) = foldl del_simp1 (mss, mk_rews thm);
   3.211 -
   3.212 -val del_simps = foldl del_simp;
   3.213 +fun del_simps(mss,thms) =
   3.214 +  orient_comb_simps del_rrule (mk_rrule mss) (mss,thms);
   3.215  
   3.216  
   3.217  (* add_congs *)
   3.218  
   3.219 -fun add_cong (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, thm) =
   3.220 +fun add_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thm) =
   3.221    let
   3.222      val (lhs, _) = Logic.dest_equals (concl_of thm) handle TERM _ =>
   3.223        raise SIMPLIFIER ("Congruence not a meta-equality", thm);
   3.224 @@ -1631,7 +1701,7 @@
   3.225  
   3.226  (* del_congs *)
   3.227  
   3.228 -fun del_cong (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, thm) =
   3.229 +fun del_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thm) =
   3.230    let
   3.231      val (lhs, _) = Logic.dest_equals (concl_of thm) handle TERM _ =>
   3.232        raise SIMPLIFIER ("Congruence not a meta-equality", thm);
   3.233 @@ -1648,7 +1718,7 @@
   3.234  
   3.235  (* add_simprocs *)
   3.236  
   3.237 -fun add_proc (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless},
   3.238 +fun add_proc (mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless},
   3.239      (name, lhs as Cterm {sign_ref, t, ...}, proc, id)) =
   3.240    (trace_term false ("Adding simplification procedure " ^ quote name ^ " for:")
   3.241        (Sign.deref sign_ref) t;
   3.242 @@ -1665,7 +1735,7 @@
   3.243  
   3.244  (* del_simprocs *)
   3.245  
   3.246 -fun del_proc (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless},
   3.247 +fun del_proc (mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless},
   3.248      (name, lhs as Cterm {t, ...}, proc, id)) =
   3.249    mk_mss (rules, congs,
   3.250      Net.delete_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
   3.251 @@ -1680,7 +1750,7 @@
   3.252  
   3.253  (* prems *)
   3.254  
   3.255 -fun add_prems (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, thms) =
   3.256 +fun add_prems (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thms) =
   3.257    mk_mss (rules, congs, procs, bounds, thms @ prems, mk_rews, termless);
   3.258  
   3.259  fun prems_of_mss (Mss {prems, ...}) = prems;
   3.260 @@ -1689,11 +1759,22 @@
   3.261  (* mk_rews *)
   3.262  
   3.263  fun set_mk_rews
   3.264 -  (Mss {rules, congs, procs, bounds, prems, mk_rews = _, termless}, mk_rews) =
   3.265 -    mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless);
   3.266 +  (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, mk) =
   3.267 +    mk_mss (rules, congs, procs, bounds, prems,
   3.268 +            {mk=mk, mk_sym= #mk_sym mk_rews, mk_eq_True= #mk_eq_True mk_rews},
   3.269 +            termless);
   3.270  
   3.271 -fun mk_rews_of_mss (Mss {mk_rews, ...}) = mk_rews;
   3.272 +fun set_mk_sym
   3.273 +  (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, mk_sym) =
   3.274 +    mk_mss (rules, congs, procs, bounds, prems,
   3.275 +            {mk= #mk mk_rews, mk_sym= mk_sym, mk_eq_True= #mk_eq_True mk_rews},
   3.276 +            termless);
   3.277  
   3.278 +fun set_mk_eq_True
   3.279 +  (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, mk_eq_True) =
   3.280 +    mk_mss (rules, congs, procs, bounds, prems,
   3.281 +            {mk= #mk mk_rews, mk_sym= #mk_sym mk_rews, mk_eq_True= mk_eq_True},
   3.282 +            termless);
   3.283  
   3.284  (* termless *)
   3.285  
   3.286 @@ -1744,18 +1825,11 @@
   3.287  
   3.288  (* mk_procrule *)
   3.289  
   3.290 -fun mk_procrule (thm as Thm {sign_ref, prop, ...}) =
   3.291 -  let
   3.292 -    val sign = Sign.deref sign_ref;
   3.293 -    val prems = Logic.strip_imp_prems prop;
   3.294 -    val concl = Logic.strip_imp_concl prop;
   3.295 -    val (lhs, _) = Logic.dest_equals concl handle TERM _ =>
   3.296 -      raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
   3.297 -    val econcl = Pattern.eta_contract concl;
   3.298 -    val (elhs, erhs) = Logic.dest_equals econcl;
   3.299 -  in case Logic.rewrite_rule_extra_vars prems elhs erhs of
   3.300 -       Some msg => (prtm true msg sign prop; [])
   3.301 -     | None => [{thm = thm, lhs = lhs, perm = false}]
   3.302 +fun mk_procrule thm =
   3.303 +  let val (_,prems,lhs,rhs,_) = decomp_simp thm
   3.304 +  in if rewrite_rule_extra_vars prems lhs rhs
   3.305 +     then (prthm true "Extra vars on rhs" thm; [])
   3.306 +     else [{thm = thm, lhs = lhs, perm = false}]
   3.307    end;
   3.308  
   3.309  
   3.310 @@ -1773,7 +1847,7 @@
   3.311  *)
   3.312  
   3.313  fun rewritec (prover,sign_reft,maxt)
   3.314 -             (mss as Mss{rules, procs, mk_rews, termless, prems, ...}) 
   3.315 +             (mss as Mss{rules, procs, termless, prems, ...}) 
   3.316               (shypst,hypst,t,ders) =
   3.317    let
   3.318        val signt = Sign.deref sign_reft;
   3.319 @@ -1969,7 +2043,7 @@
   3.320                                                    (Sign.deref sign_ref) s1; mss)
   3.321               else let val thm = assume (Cterm{sign_ref=sign_ref, t=s1, 
   3.322                                                T=propT, maxidx= ~1})
   3.323 -                  in add_simp(add_prems(mss,[thm]), thm) end
   3.324 +                  in safe_add_simps(add_prems(mss,[thm]), [thm]) end
   3.325             val (shyps2,hyps2,u1,ders2) = try_botc mss1 (shyps1,hyps1,u,ders1)
   3.326             val hyps3 = if gen_mem (op aconv) (s1, hyps1)
   3.327                         then hyps2 else hyps2\s1