Isar.init;
authorwenzelm
Mon, 05 Jan 2009 00:13:11 +0100
changeset 29349 b49d8501720a
parent 29348 28b0652aabd8
child 29350 c7735554d291
Isar.init;
src/Pure/Isar/isar_syn.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
--- 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 ());