--- 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