# HG changeset patch
# User wenzelm
# Date 924779782 -7200
# Node ID 3e5d450c2b31e8d4fe2e0246acba533f740b0123
# Parent  324a4051ff7b2ca1da213b6b19bc54c9c25e6435
switch_theory: Context.pass;

diff -r 324a4051ff7b -r 3e5d450c2b31 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Thu Apr 22 13:04:50 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Thu Apr 22 13:16:22 1999 +0200
@@ -337,9 +337,8 @@
 
 (* context switch *)
 
-fun switch_theory load name =
-  Toplevel.init_theory
-    (fn () => (Context.save load name; ThyInfo.get_theory name)) (K ());
+fun switch_theory load s =
+  Toplevel.init_theory (fn () => (the (#2 (Context.pass None load s)))) (K ());
 
 val context = switch_theory ThyInfo.use_thy;
 val update_context = switch_theory ThyInfo.update_thy;