src/HOL/Statespace/state_space.ML

--- a/src/HOL/Statespace/state_space.ML	Sun Sep 28 14:46:51 2008 +0200
+++ b/src/HOL/Statespace/state_space.ML	Mon Sep 29 10:58:01 2008 +0200
@@ -352,8 +352,7 @@
   thy
   |> TheoryTarget.init name
   |> (fn lthy => LocalTheory.declaration (decl lthy) lthy)
-  |> LocalTheory.exit
-  |> ProofContext.theory_of;
+  |> LocalTheory.exit_global;
 
 fun parent_components thy (Ts, pname, renaming) =
   let