src/Tools/isac/Specify/cas-command.sml
changeset 60782 e797d1bdfe37
parent 60779 fabe6923e819
     1.1 --- a/src/Tools/isac/Specify/cas-command.sml	Mon Dec 11 16:18:42 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/cas-command.sml	Mon Dec 11 17:26:30 2023 +0100
     1.3 @@ -11,9 +11,9 @@
     1.4  
     1.5  (*/----- from isac_test for Minisubpbl*)
     1.6    val input_: References.T -> (term * term list) list ->
     1.7 -    Problem.id * I_Model.T_POS * MethodC.id * I_Model.T_POS * Pre_Conds.T * Proof.context
     1.8 +    Problem.id * I_Model.T * MethodC.id * I_Model.T * Pre_Conds.T * Proof.context
     1.9    val dtss2itm_: Model_Pattern.T -> term * term list ->
    1.10 -    int list * bool * Model_Def.m_field * (I_Model.feedback_POS * Position.T)
    1.11 +    int list * bool * Model_Def.m_field * (I_Model.feedback * Position.T)
    1.12    val flattup2: 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e
    1.13  (*\----- from isac_test for Minisubpbl*)
    1.14  
    1.15 @@ -36,7 +36,7 @@
    1.16    		(#1: (term * term) -> term) o
    1.17    		(#2: Model_Pattern.single -> (term * term))) model)
    1.18    in
    1.19 -    ([1], true, f, (I_Model.Cor_POS (d, ts), Position.none))
    1.20 +    ([1], true, f, (I_Model.Cor (d, ts), Position.none))
    1.21    end
    1.22  
    1.23  fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)