1.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Tue Jun 23 18:10:39 2009 +0200
     1.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Tue Jun 23 21:03:31 2009 +0200
     1.3 @@ -184,7 +184,7 @@
     1.4      val subgoal = Thm.term_of csubgoal;
     1.5    in
     1.6   (let
     1.7 -    val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_datatypes) sign;
     1.8 +    val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_all) sign;
     1.9      val concl = Logic.strip_imp_concl subgoal;
    1.10      val ic_str = delete_ul_string(Syntax.string_of_term_global sign (IntC sign concl));
    1.11      val ia_str = delete_ul_string(Syntax.string_of_term_global sign (IntA sign concl));