tuned printed type names, according to ML;
authorwenzelm
Fri, 27 Aug 2010 17:02:19 +0200
changeset 38804 99cc7e748ab4
parent 38803 38b68972721b
child 38805 b09d8603f865
tuned printed type names, according to ML;
src/Pure/config.ML
--- a/src/Pure/config.ML	Fri Aug 27 16:32:11 2010 +0200
+++ b/src/Pure/config.ML	Fri Aug 27 17:02:19 2010 +0200
@@ -41,8 +41,8 @@
   | print_value (Int i) = signed_string_of_int i
   | print_value (String s) = quote s;
 
-fun print_type (Bool _) = "boolean"
-  | print_type (Int _) = "integer"
+fun print_type (Bool _) = "bool"
+  | print_type (Int _) = "int"
   | print_type (String _) = "string";
 
 fun same_type (Bool _) (Bool _) = true