1.1 --- a/src/Tools/isac/MathEngBasic/method.sml Mon Jun 21 20:06:12 2021 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/method.sml Mon Jun 21 21:53:23 2021 +0200
1.3 @@ -126,11 +126,11 @@
1.4 (fn (name, (id, (((source, maa), program), model_input))) => Toplevel.theory (fn thy =>
1.5 let
1.6 val metID = References_Def.explode_id id;
1.7 - val eval_input =
1.8 + val set_data =
1.9 ML_Context.expression (Input.pos_of source)
1.10 (ml "Theory.setup (MethodC.set_data (" @ ML_Lex.read_source source @ ml "))")
1.11 |> Context.theory_map;
1.12 - val input = the_data (eval_input thy);
1.13 + val input = the_data (set_data thy);
1.14 val thm =
1.15 (case program of
1.16 NONE => @{thm refl}