src/HOL/Statespace/state_space.ML

   val valuetypesN : string
 
   val namespace_definition :
      bstring ->
      typ ->
-     Expression.expression ->
+     (xstring, string) Expression.expr * (binding * string option * mixfix) list ->
      string list -> string list -> theory -> theory
 
   val define_statespace :
      string list ->
      string ->

       (make_namespace_data declinfo distinctthm silent) ctxt
   end;
 
 val get_silent = #silent o NameSpaceData.get;
 
+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_cmd I name expr []
+   |> Expression.sublocale_cmd I (name, Position.none) (expression_no_pos expr) []
    |> Proof.global_terminal_proof
          (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), NONE)
    |> Proof_Context.theory_of
 
 fun add_locale name expr elems thy =

   |> snd
   |> Local_Theory.exit;
 
 fun add_locale_cmd name expr elems thy =
   thy
-  |> Expression.add_locale_cmd I (Binding.name name) Binding.empty expr elems
+  |> Expression.add_locale_cmd I (Binding.name name) Binding.empty (expression_no_pos expr) elems
   |> snd
   |> Local_Theory.exit;
 
 type statespace_info =
  {args: (string * sort) list, (* type arguments *)