1.1 --- a/src/Tools/isac/Test_Code/test-code.sml	Mon Oct 31 18:28:36 2022 +0100
     1.2 +++ b/src/Tools/isac/Test_Code/test-code.sml	Mon Nov 07 17:37:20 2022 +0100
     1.3 @@ -43,12 +43,12 @@
     1.4    in
     1.5      case form of
     1.6        Ctree.Form t => Test_Out.FormKF (UnparseC.term t)
     1.7 -    | Ctree.ModSpec (_, p_, _, gfr, pre, _) =>
     1.8 +    | Ctree.ModSpec (_, p_, _, gfr, where_, _) =>
     1.9        Test_Out.PpcKF (
    1.10          (case p_ of Pos.Pbl => Test_Out.Problem []
    1.11            | Pos.Met => Test_Out.MethodC []
    1.12            | _ => raise ERROR "TESTg_form: uncovered case",
    1.13 - 			P_Model.from (Proof_Context.theory_of ctxt) gfr pre))
    1.14 + 			P_Model.from (Proof_Context.theory_of ctxt) gfr where_))
    1.15     end
    1.16  (* for quick test-print-out, until 'type inout' is removed *)
    1.17  fun f2str (Test_Out.FormKF cterm') = cterm'