author | mengj |
Thu, 23 Feb 2006 13:00:18 +0100 | |
changeset 19130 | b23479b80828 |
parent 19129 | b66dff8ab7e9 |
child 19131 | 06b6f5f8e4cb |
--- a/src/HOL/Tools/res_hol_clause.ML Thu Feb 23 12:59:01 2006 +0100 +++ b/src/HOL/Tools/res_hol_clause.ML Thu Feb 23 13:00:18 2006 +0100 @@ -513,7 +513,7 @@ datatype type_level = T_FULL | T_PARTIAL | T_CONST | T_NONE; -val typ_level = ref T_PARTIAL; +val typ_level = ref T_FULL; fun full_types () = (typ_level:=T_FULL); fun partial_types () = (typ_level:=T_PARTIAL);