diff -r abe867c29e55 -r dea60d052923 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Sat Dec 18 14:02:14 2010 +0100
+++ b/src/HOL/Statespace/state_space.ML	Sat Dec 18 18:43:13 2010 +0100
@@ -145,7 +145,7 @@
 
 fun prove_interpretation_in ctxt_tac (name, expr) thy =
    thy
-   |> Expression.sublocale_cmd name expr
+   |> Expression.sublocale_cmd name expr []
    |> Proof.global_terminal_proof
          (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), NONE)
    |> ProofContext.theory_of