--- a/src/HOLCF/IOA/Modelcheck/MuIOA.ML Mon Oct 02 14:58:39 2000 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.ML Mon Oct 02 14:59:04 2000 +0200
@@ -164,6 +164,8 @@
fun mk_sim_oracle (sign, SimOracleExn (subgoal,thl)) =
(let
+ val weak_case_congs = DatatypePackage.weak_case_congs_of_sg sign;
+
val concl = (Logic.strip_imp_concl subgoal);
val ic_str = delete_ul_string(Sign.string_of_term sign (IntC sign concl));
@@ -258,12 +260,14 @@
by (REPEAT (rtac impI 1));
by (REPEAT (dtac eq_reflection 1));
(* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
-by (full_simp_tac ((simpset() delcongs [if_weak_cong]
+by (full_simp_tac ((simpset() delcongs (if_weak_cong :: weak_case_congs)
delsimps [not_iff,split_part])
addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
rename_simps @ ioa_simps @ asig_simps)) 1);
-by (full_simp_tac (Mucke_ss delcongs [if_weak_cong] delsimps [not_iff,split_part]) 1);
-by (REPEAT (if_full_simp_tac (simpset() delcongs [if_weak_cong] delsimps [not_iff,split_part]) 1));
+by (full_simp_tac
+ (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1);
+by (REPEAT (if_full_simp_tac
+ (simpset() delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
by (call_mucke_tac 1);
(* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
by (atac 1);