--- a/src/Pure/Isar/isar_syn.ML Mon Jan 05 00:12:49 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML Mon Jan 05 00:13:11 2009 +0100
@@ -774,7 +774,7 @@
val _ =
OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" K.control
- (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.init_point));
+ (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.init));
val _ =
OuterSyntax.improper_command "linear_undo" "undo commands" K.control
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Jan 05 00:12:49 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Jan 05 00:13:11 2009 +0100
@@ -144,7 +144,7 @@
(warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
tell_file_retracted (ThyLoad.thy_path name))
else ();
- val _ = Isar.init_point ();
+ val _ = Isar.init ();
in () end;
@@ -156,7 +156,7 @@
(sync_thy_loader ();
tell_clear_goals ();
tell_clear_response ();
- Isar.init_point ();
+ Isar.init ();
welcome ());
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Jan 05 00:12:49 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Jan 05 00:13:11 2009 +0100
@@ -242,7 +242,7 @@
(sync_thy_loader ();
tell_clear_goals ();
tell_clear_response ();
- Isar.init_point ();
+ Isar.init ();
welcome ());