1.1 --- a/src/HOL/Statespace/state_space.ML	Wed Sep 23 13:17:17 2009 +0200
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Wed Sep 23 13:31:38 2009 +0200
     1.3 @@ -321,17 +321,14 @@
     1.4       |> interprete_parent name dist_thm_full_name parent_expr
     1.5    end;
     1.6  
     1.7 -fun encode_dot x =
     1.8 -    if x= #"." then #"_" else x;
     1.9 +fun encode_dot x = if x= #"." then #"_" else x;
    1.10  
    1.11  fun encode_type (TFree (s, _)) = s
    1.12    | encode_type (TVar ((s,i),_)) = "?" ^ s ^ string_of_int i
    1.13    | encode_type (Type (n,Ts)) =
    1.14        let
    1.15          val Ts' = fold1' (fn x => fn y => x ^ "_" ^ y) (map encode_type Ts) "";
    1.16 -        val n' = if n = "*" then "Prod" else
    1.17 -                   if n = "+" then "Sum" else
    1.18 -                     String.map encode_dot n;
    1.19 +        val n' = String.map encode_dot n;
    1.20        in if Ts'="" then n' else Ts' ^ "_" ^ n' end;
    1.21  
    1.22  fun project_name T = projectN ^"_"^encode_type T;
    1.23 @@ -695,4 +692,4 @@
    1.24  
    1.25  end;
    1.26  
    1.27 -end;
    1.28 +end;
    1.29 \ No newline at end of file