src/Tools/Code/code_runtime.ML
changeset 62716 d80b9f4990e4
parent 62607 43d282be7350
child 62876 507c90523113
     1.1 --- a/src/Tools/Code/code_runtime.ML	Sat Mar 26 14:27:58 2016 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Sat Mar 26 16:14:46 2016 +0100
     1.3 @@ -524,6 +524,7 @@
     1.4      allStruct    = #allStruct ML_Env.name_space,
     1.5      allSig       = #allSig ML_Env.name_space,
     1.6      allFunct     = #allFunct ML_Env.name_space},
     1.7 +  print_depth = NONE,
     1.8    here = #here ML_Env.context,
     1.9    print = #print ML_Env.context,
    1.10    error = #error ML_Env.context};