1.1 --- a/src/Tools/isac/Specify/cas-command.sml	Sat Feb 04 17:00:25 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/cas-command.sml	Tue Feb 07 17:25:09 2023 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4  
     1.5  fun input_ ((dI, pI, mI): References.T) dtss = (*WN110515 reconsider thy..ctxt*)
     1.6    let
     1.7 -    val thy = ThyC.get_theory dI
     1.8 +    val thy = Know_Store.get_via_last_thy dI
     1.9      val ctxt = Proof_Context.init_global thy
    1.10  	  val {model, ...} = Problem.from_store ctxt pI
    1.11  	  val its_ = map (dtss2itm_ model) dtss (*([1],true,"#Given",Cor (...))*)