changeset 37198 | 3af985b10550 |
parent 36960 | 01594f816e3a |
child 37390 | 8781d80026fc |
--- a/src/HOL/Tools/inductive_codegen.ML Sun May 30 18:23:50 2010 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Sun May 30 21:34:19 2010 +0200 @@ -836,7 +836,7 @@ [str "]"]), Pretty.brk 1, str "| NONE => NONE);"]) ^ "\n\nend;\n"; - val _ = ML_Context.eval_in (SOME ctxt) false Position.none s; + val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s; val values = Config.get ctxt random_values; val bound = Config.get ctxt depth_bound; val start = Config.get ctxt depth_start;