src/Tools/isac/MathEngBasic/method.sml
changeset 60314 1cf9c607fa6a
parent 60307 d692abd52098
child 60339 0d22a6bf1fc6
     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}