# HG changeset patch
# User wenzelm
# Date 918246380 -3600
# Node ID dbaf79ac2ff90a3062440aff2059364d0c7f42c6
# Parent  935f183bf406f7239dbcc343eac05b2f70bc6680
made MLWorks happy;

diff -r 935f183bf406 -r dbaf79ac2ff9 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Fri Feb 05 21:14:17 1999 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Fri Feb 05 21:26:20 1999 +0100
@@ -255,9 +255,9 @@
 
 (* context switch *)
 
-fun switch_theory require name =
+fun switch_theory load name =
   Toplevel.init_theory
-    (fn () => (Context.save require name; ThyInfo.get_theory name)) (K ());
+    (fn () => (Context.save load name; ThyInfo.get_theory name)) (K ());
 
 val context = switch_theory ThyInfo.use_thy;
 val update_context = switch_theory ThyInfo.update_thy;