1.1 --- a/test/Tools/isac/Specify/i-model.sml	Fri Dec 01 06:08:22 2023 +0100
     1.2 +++ b/test/Tools/isac/Specify/i-model.sml	Tue Dec 05 18:15:45 2023 +0100
     1.3 @@ -170,14 +170,15 @@
     1.4  (*+*)val [Free ("q_0", _)] = all;
     1.5  
     1.6  (**)val ("", itm) =(**)
     1.7 - (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*);
     1.8 + (*case*) is_notyet_input ctxt (OLD_to_POS i_model) all ori' m_patt (*of*);
     1.9  
    1.10 -(*+*)val (2, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]), (Free ("q_q", _), [Free ("q_0", _)]))) = itm
    1.11 +(*+*)val (2, [1], true, "#Given", (Cor_POS (Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]), _)) = itm
    1.12  (*\\------------------ step into check_single ----------------------------------------------//*)
    1.13  val return_check_single = Add itm;
    1.14  
    1.15  "~~~~~ from fun check_single \<longrightarrow>fun by_Add_ , return:"; val (I_Model.Add i_single) = (return_check_single);
    1.16 -	          val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model
    1.17 +	          val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt)
    1.18 +	            (I_Model.TEST_to_OLD_single i_single) i_model
    1.19              val tac' = I_Model.make_tactic m_field (ct, i_model')
    1.20  ;
    1.21  (*+*)if I_Model.to_string ctxt i_model' = "[\n" ^