src/Pure/config.ML
changeset 38804 99cc7e748ab4
parent 36787 f60e4dd6d76f
child 39116 f14735a88886
     1.1 --- a/src/Pure/config.ML	Fri Aug 27 16:32:11 2010 +0200
     1.2 +++ b/src/Pure/config.ML	Fri Aug 27 17:02:19 2010 +0200
     1.3 @@ -41,8 +41,8 @@
     1.4    | print_value (Int i) = signed_string_of_int i
     1.5    | print_value (String s) = quote s;
     1.6  
     1.7 -fun print_type (Bool _) = "boolean"
     1.8 -  | print_type (Int _) = "integer"
     1.9 +fun print_type (Bool _) = "bool"
    1.10 +  | print_type (Int _) = "int"
    1.11    | print_type (String _) = "string";
    1.12  
    1.13  fun same_type (Bool _) (Bool _) = true