src/HOLCF/IOA/Modelcheck/MuIOA.thy
changeset 37391 476270a6c2dc
parent 37140 6ba1b0ef0cc4
child 37678 0040bafffdef
     1.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Thu Jun 10 12:24:02 2010 +0200
     1.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Thu Jun 10 12:24:03 2010 +0200
     1.3 @@ -34,9 +34,9 @@
     1.4  
     1.5  exception malformed;
     1.6  
     1.7 -fun fst_type (Type("*",[a,_])) = a |
     1.8 +fun fst_type (Type(@{type_name "*"},[a,_])) = a |
     1.9  fst_type _ = raise malformed; 
    1.10 -fun snd_type (Type("*",[_,a])) = a |
    1.11 +fun snd_type (Type(@{type_name "*"},[_,a])) = a |
    1.12  snd_type _ = raise malformed;
    1.13  
    1.14  fun element_type (Type("set",[a])) = a |
    1.15 @@ -121,10 +121,10 @@
    1.16  
    1.17  fun delete_ul_string s = implode(delete_ul (explode s));
    1.18  
    1.19 -fun type_list_of sign (Type("*",a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) |
    1.20 +fun type_list_of sign (Type(@{type_name "*"},a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) |
    1.21  type_list_of sign a = [(Syntax.string_of_typ_global sign a)];
    1.22  
    1.23 -fun structured_tuple l (Type("*",s::t::_)) =
    1.24 +fun structured_tuple l (Type(@{type_name "*"},s::t::_)) =
    1.25  let
    1.26  val (r,str) = structured_tuple l s;
    1.27  in