author | wenzelm |
Fri, 05 Feb 1999 21:26:20 +0100 | |
changeset 6253 | dbaf79ac2ff9 |
parent 6252 | 935f183bf406 |
child 6254 | f6335d319e9f |
--- 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;