src/Pure/Isar/isar_thy.ML
changeset 6253 dbaf79ac2ff9
parent 6246 0aa2e536bc20
child 6266 a5f9fa6b6d7c
equal deleted inserted replaced
6252:935f183bf406 6253:dbaf79ac2ff9
   253 fun theory spec = Toplevel.init_theory (begin_theory spec) end_theory;
   253 fun theory spec = Toplevel.init_theory (begin_theory spec) end_theory;
   254 
   254 
   255 
   255 
   256 (* context switch *)
   256 (* context switch *)
   257 
   257 
   258 fun switch_theory require name =
   258 fun switch_theory load name =
   259   Toplevel.init_theory
   259   Toplevel.init_theory
   260     (fn () => (Context.save require name; ThyInfo.get_theory name)) (K ());
   260     (fn () => (Context.save load name; ThyInfo.get_theory name)) (K ());
   261 
   261 
   262 val context = switch_theory ThyInfo.use_thy;
   262 val context = switch_theory ThyInfo.use_thy;
   263 val update_context = switch_theory ThyInfo.update_thy;
   263 val update_context = switch_theory ThyInfo.update_thy;
   264 
   264 
   265 
   265