src/Pure/Isar/toplevel.ML

 fun copy_node true (Theory thy) = Theory (Theory.copy thy)
   | copy_node _ node = node;
 
 fun interruptible f x =
   let val y = ref (None: node History.T option);
-  in exhibit_interrupt (fn () => y := Some (f x)) (); the (! y) end;
+  in raise_interrupt (fn () => y := Some (f x)) (); the (! y) end;
 
 val rollback = ERROR_MESSAGE "Stale signature encountered after succesful execution!";
 
 fun return (result, None) = result
   | return (result, Some exn) = raise FAILURE (result, exn);

   | apply_tr _ Exit (State (Some (node, (exit, _)))) =
       (exit (History.current node); State None)
   | apply_tr _ Kill (State None) = raise UNDEF
   | apply_tr _ Kill (State (Some (node, (_, kill)))) =
       (kill (History.current node); State None)
-  | apply_tr int (Keep f) state = (exhibit_interrupt (f int) state; state)
+  | apply_tr int (Keep f) state = (raise_interrupt (f int) state; state)
   | apply_tr _ (History _) (State None) = raise UNDEF
   | apply_tr _ (History f) (State (Some (node, term))) = State (Some (f node, term))
   | apply_tr int (MapCurrent f) state = node_trans int false f state
   | apply_tr int (AppCurrent f) state = node_trans int true f state;
 

     None => (writeln "\nInterrupt."; raw_loop src)
   | Some None => ()
   | Some (Some (tr, src')) => if >> tr then raw_loop src' else ());
 
 
-fun loop src = mask_interrupt raw_loop src;
+fun loop src = ignore_interrupt raw_loop src;
 
 
 end;