# HG changeset patch
# User wenzelm
# Date 970491544 -7200
# Node ID 98ddd0138cbf98b7a0d76746b3378ac1a445bfed
# Parent  86269867de34f6e4b1c52cb08635c55f4a66cf9e
delcongs weak_case_congs;

diff -r 86269867de34 -r 98ddd0138cbf src/HOLCF/IOA/Modelcheck/MuIOA.ML
--- 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);