# HG changeset patch
# User mengj
# Date 1140696018 -3600
# Node ID b23479b808288ab5f0630761368ba4f4039da19c
# Parent  b66dff8ab7e9759c0955bb7eb90ad2f290c21436
Default type level is T_FULL now.

diff -r b66dff8ab7e9 -r b23479b80828 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);