--- a/src/HOL/Statespace/state_space.ML Sat Nov 14 08:45:51 2015 +0100
+++ b/src/HOL/Statespace/state_space.ML Sat Nov 14 08:45:51 2015 +0100
@@ -127,7 +127,7 @@
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