1.1 --- a/src/Tools/isac/Specify/cas-command.sml	Fri Dec 01 06:08:22 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/cas-command.sml	Tue Dec 05 18:15:45 2023 +0100
     1.3 @@ -9,13 +9,17 @@
     1.4    type T = CAS_Def.T
     1.5    val input : term -> (Ctree.ctree * SpecificationC.T) option
     1.6    val is_from: TermC.as_string -> Formalise.T -> bool
     1.7 -\<^isac_test>\<open>
     1.8 +
     1.9 +(*/----- from isac_test for Minisubpbl*)
    1.10    val input_: References.T -> (term * term list) list ->
    1.11 -    Problem.id * I_Model.T * MethodC.id * I_Model.T * Pre_Conds.T * Proof.context
    1.12 -
    1.13 +    Problem.id * I_Model.T_POS * MethodC.id * I_Model.T_POS * Pre_Conds.T * Proof.context
    1.14    val dtss2itm_: Model_Pattern.T -> term * term list ->
    1.15      int list * bool * string * I_Model.feedback (*I_Model.single'*)
    1.16    val flattup2: 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e
    1.17 +(*\----- from isac_test for Minisubpbl*)
    1.18 +
    1.19 +\<^isac_test>\<open>
    1.20 +(*put "from isac_test for Minisubpbl" here*)
    1.21  \<close>
    1.22  end
    1.23  
    1.24 @@ -62,7 +66,7 @@
    1.25  	  val mits = map flattup2 its
    1.26  	  val (_, where_) = Pre_Conds.check ctxt where_rls where_ (model, I_Model.OLD_to_POS mits)
    1.27      val ctxt = Proof_Context.init_global thy
    1.28 -  in (pI, pits, mI, mits, where_, ctxt) end;
    1.29 +  in (pI, I_Model.OLD_to_POS pits, mI, I_Model.OLD_to_POS mits, where_, ctxt) end;
    1.30  
    1.31  (* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *)
    1.32  fun input hdt =
    1.33 @@ -79,10 +83,11 @@
    1.34  	        val (pt,_) = Ctree.cappend_problem Ctree.e_ctree [] (Istate_Def.empty, ContextC.empty)
    1.35  		        ([], References.empty) ([], References.empty, hdt, ctxt)
    1.36  	        val pt = Ctree.update_spec pt [] spec
    1.37 -	        val pt = Ctree.update_pbl pt [] pits
    1.38 -	        val pt = Ctree.update_met pt [] mits
    1.39 +	        val pt = Ctree.update_pbl pt [] (I_Model.TEST_to_OLD pits)
    1.40 +	        val pt = Ctree.update_met pt [] (I_Model.TEST_to_OLD mits)
    1.41  	      in
    1.42 -	        SOME (pt, (true, Pos.Met, hdt, mits, where_, spec) : SpecificationC.T)
    1.43 +(*quick and dirty------------------------vvvvvvvvvvvvvvvvvvv-----*)
    1.44 +	        SOME (pt, (true, Pos.Met, hdt, I_Model.TEST_to_OLD mits, where_, spec) : SpecificationC.T)
    1.45  	      end
    1.46    end
    1.47