1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Mon Jun 21 20:06:12 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Mon Jun 21 21:53:23 2021 +0200
     1.3 @@ -205,11 +205,11 @@
     1.4          let
     1.5            val ctxt = Proof_Context.init_global thy;
     1.6            val Const (c, _) = Proof_Context.read_const {proper = true, strict = true} ctxt const;
     1.7 -          val eval_ml =
     1.8 +          val set_data =
     1.9              ML_Context.expression (Input.pos_of source)
    1.10                (ml "Theory.setup (Eval_Def.set_data (" @ ML_Lex.read_source source @ ml "))")
    1.11              |> Context.theory_map;
    1.12 -          val eval = Eval_Def.the_data (eval_ml thy);
    1.13 +          val eval = Eval_Def.the_data (set_data thy);
    1.14          in KEStore_Elems.add_calcs [(calcID, (c, eval))] thy end)))
    1.15  
    1.16  in end;