Default type level is T_FULL now.
authormengj
Thu, 23 Feb 2006 13:00:18 +0100
changeset 19130 b23479b80828
parent 19129 b66dff8ab7e9
child 19131 06b6f5f8e4cb
Default type level is T_FULL now.
src/HOL/Tools/res_hol_clause.ML
--- 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);