--- a/src/Pure/Isar/class_target.ML Thu Jul 01 16:54:42 2010 +0200
+++ b/src/Pure/Isar/class_target.ML Thu Jul 01 16:54:44 2010 +0200
@@ -450,7 +450,7 @@
(* target *)
-val sanitize_name = (*FIXME*)
+val sanitize_name = (*necessary as long as "dirty" type identifiers are permitted*)
let
fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s
orelse s = "'" orelse s = "_";
@@ -465,9 +465,7 @@
explode #> scan_valids #> implode
end;
-fun type_name "Product_Type.*" = "prod"
- | type_name "Sum_Type.+" = "sum"
- | type_name s = sanitize_name (Long_Name.base_name s);
+val type_name = sanitize_name o Long_Name.base_name;
fun resort_terms pp algebra consts constraints ts =
let