Undo errornous commit of Statespace change
authorhoelzl
Wed, 23 Sep 2009 13:31:38 +0200
changeset 32651 af55ccf865a4
parent 32650 34bfa2492298
child 32653 7feb35deb6f6
Undo errornous commit of Statespace change
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