src/HOL/Statespace/state_space.ML

 fun expression_no_pos (expr, fixes) : Expression.expression =
   (map (fn (name, inst) => ((name, Position.none), inst)) expr, fixes);
 
 fun prove_interpretation_in ctxt_tac (name, expr) thy =
    thy
-   |> Expression.sublocale_global_cmd (name, Position.none) (expression_no_pos expr) []
+   |> Interpretation.sublocale_global_cmd (name, Position.none) (expression_no_pos expr) []
    |> Proof.global_terminal_proof
          ((Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), Position.no_range), NONE)
    |> Proof_Context.theory_of
 
 fun add_locale name expr elems thy =