# HG changeset patch
# User hoelzl
# Date 1253705498 -7200
# Node ID af55ccf865a49f059f4709840bbf823f6cc43af7
# Parent  34bfa2492298b709a4aa52b49e765ee2e3ded997
Undo errornous commit of Statespace change

diff -r 34bfa2492298 -r af55ccf865a4 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Wed Sep 23 13:17:17 2009 +0200
+++ b/src/HOL/Statespace/state_space.ML	Wed Sep 23 13:31:38 2009 +0200
@@ -321,17 +321,14 @@
      |> interprete_parent name dist_thm_full_name parent_expr
   end;
 
-fun encode_dot x =
-    if x= #"." then #"_" else x;
+fun encode_dot x = if x= #"." then #"_" else x;
 
 fun encode_type (TFree (s, _)) = s
   | encode_type (TVar ((s,i),_)) = "?" ^ s ^ string_of_int i
   | encode_type (Type (n,Ts)) =
       let
         val Ts' = fold1' (fn x => fn y => x ^ "_" ^ y) (map encode_type Ts) "";
-        val n' = if n = "*" then "Prod" else
-                   if n = "+" then "Sum" else
-                     String.map encode_dot n;
+        val n' = String.map encode_dot n;
       in if Ts'="" then n' else Ts' ^ "_" ^ n' end;
 
 fun project_name T = projectN ^"_"^encode_type T;
@@ -695,4 +692,4 @@
 
 end;
 
-end;
+end;
\ No newline at end of file