# HG changeset patch
# User haftmann
# Date 1276165567 -7200
# Node ID 6ff1fce8e156d1591e1e685df31a4c91063e83a2
# Parent  b39f640b94d44e8a78aeccee5431b92707ecbf98
adjust popular symbolic type constructors

diff -r b39f640b94d4 -r 6ff1fce8e156 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Thu Jun 10 12:25:14 2010 +0200
+++ b/src/Pure/Isar/class_target.ML	Thu Jun 10 12:26:07 2010 +0200
@@ -465,8 +465,8 @@
     explode #> scan_valids #> implode
   end;
 
-fun type_name "*" = "prod"
-  | type_name "+" = "sum"
+fun type_name "Product_Type.*" = "prod"
+  | type_name "Sum_Type.+" = "sum"
   | type_name s = sanitize_name (Long_Name.base_name s);
 
 fun resort_terms pp algebra consts constraints ts =