1.1 --- a/src/Tools/isac/Test_Code/test-code.sml	Wed Jan 11 11:38:01 2023 +0100
     1.2 +++ b/src/Tools/isac/Test_Code/test-code.sml	Wed Jan 25 15:52:33 2023 +0100
     1.3 @@ -57,8 +57,9 @@
     1.4  (* create a calc-tree *)
     1.5  fun init_calc ctxt [(model, refs as (thy_id, _, _))] =
     1.6    let
     1.7 -    val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global
     1.8 -    val ((pt, p), tacis) = Step_Specify.nxt_specify_init_calc ctxt (model, refs)
     1.9 +(*old* )val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global
    1.10 +( *new*)val thy = thy_id |> ThyC.get_theory_PIDE ctxt  (*^^^^^^^^^^^^^^^^^^^^^^^^^ misleading*)
    1.11 +    val ((pt, p), tacis) = Step_Specify.nxt_specify_init_calc_PIDE thy (model, refs)
    1.12  	  val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
    1.13  	  val f = TESTg_form ctxt (pt,p)
    1.14    in (p, []:NEW, f, tac, Celem.Sundef, pt) end