# HG changeset patch
# User wenzelm
# Date 1282921339 -7200
# Node ID 99cc7e748ab46ef945244ef2a6fcf6e017a259c1
# Parent  38b68972721bbe0abe5f8cf127a170a9fe6515da
tuned printed type names, according to ML;

diff -r 38b68972721b -r 99cc7e748ab4 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