1.1 --- a/src/Tools/isac/Specify/cas-command.sml	Sun Aug 27 17:56:50 2023 +0200
     1.2 +++ b/src/Tools/isac/Specify/cas-command.sml	Tue Aug 29 08:35:46 2023 +0200
     1.3 @@ -41,30 +41,6 @@
     1.4  fun is_from (hdf : TermC.as_string) ((fmz_, spec) : Formalise.T) =
     1.5    hdf <> "" andalso fmz_ = [] andalso spec = References.empty
     1.6  
     1.7 -(*T_TESTold* )
     1.8 -fun input_ ((dI, pI, mI): References.T) dtss = (*WN110515 reconsider thy..ctxt*)
     1.9 -  let
    1.10 -    val thy = Know_Store.get_via_last_thy dI
    1.11 -    val ctxt = Proof_Context.init_global thy
    1.12 -	  val {model, ...} = Problem.from_store ctxt pI
    1.13 -	  val its_ = map (dtss2itm_ model) dtss (*([1],true,"#Given",Cor (...))*)
    1.14 -	  val its = O_Model.add_enumerate its_
    1.15 -	  val pits = map flattup2 its
    1.16 -	  val (pI, mI) =
    1.17 -      if mI <> ["no_met"]
    1.18 -      then (pI, mI)
    1.19 -		  else
    1.20 -        case Refine.problem thy pI pits of
    1.21 -			    SOME (pI, _) => (pI, (hd o #solve_mets o Problem.from_store ctxt) pI)
    1.22 -			  | NONE => (pI, (hd o #solve_mets o Problem.from_store ctxt) pI)
    1.23 -	  val {model, where_, where_rls, ...} = MethodC.from_store ctxt mI
    1.24 -	  val its_ = map (dtss2itm_ model) dtss (*([1],true,"#Given",Cor (...))*)
    1.25 -	  val its = O_Model.add_enumerate its_
    1.26 -	  val mits = map flattup2 its
    1.27 -	  val (_, where_) = Pre_Conds.check ctxt where_rls where_ mits 0
    1.28 -    val ctxt = Proof_Context.init_global thy
    1.29 -  in (pI, pits, mI, mits, where_, ctxt) end;
    1.30 -( *T_TEST**)
    1.31  fun input_ ((dI, pI, mI): References.T) dtss = (*WN110515 reconsider thy..ctxt*)
    1.32    let
    1.33      val thy = Know_Store.get_via_last_thy dI
    1.34 @@ -87,7 +63,6 @@
    1.35  	  val (_, where_) = Pre_Conds.check ctxt where_rls where_ (model, I_Model.OLD_to_TEST mits)
    1.36      val ctxt = Proof_Context.init_global thy
    1.37    in (pI, pits, mI, mits, where_, ctxt) end;
    1.38 -(*T_TESTnew*)
    1.39  
    1.40  (* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *)
    1.41  fun input hdt =