equal
deleted
inserted
replaced
127 fun determine_type ctxt s = |
127 fun determine_type ctxt s = |
128 let |
128 let |
129 val return = Unsynchronized.ref "return" |
129 val return = Unsynchronized.ref "return" |
130 val context : ML_Compiler0.context = |
130 val context : ML_Compiler0.context = |
131 {name_space = #name_space ML_Env.context, |
131 {name_space = #name_space ML_Env.context, |
|
132 print_depth = SOME 1000000, |
132 here = #here ML_Env.context, |
133 here = #here ML_Env.context, |
133 print = fn r => return := r, |
134 print = fn r => return := r, |
134 error = #error ML_Env.context} |
135 error = #error ML_Env.context} |
135 val _ = |
136 val _ = |
136 Context.setmp_thread_data (SOME (Context.Proof ctxt)) |
137 Context.setmp_thread_data (SOME (Context.Proof ctxt)) |