# HG changeset patch
# User wenzelm
# Date 964954233 -7200
# Node ID 3ac87f80186d5b233259eddffd146ccedd62064d
# Parent  8645b041336610e2025b30a09be97f3d7ccffb6f
ThmDeps.enable;

diff -r 8645b0413366 -r 3ac87f80186d src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Sun Jul 30 12:50:07 2000 +0200
+++ b/src/Pure/Interface/proof_general.ML	Sun Jul 30 12:50:33 2000 +0200
@@ -206,7 +206,7 @@
 
 local structure P = OuterParse and K = OuterSyntax.Keyword in
 
-val old_undoP =	(* FIXME same name for compatibility with PG/Isabelle99 *)
+val old_undoP = (* FIXME same name for compatibility with PG/Isabelle99 *)
   OuterSyntax.improper_command "undo" "undo last command (no output)" K.control
     (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
 
@@ -258,7 +258,9 @@
   setup_thy_loader ();
   print_mode := [proof_generalN];
   set quick_and_dirty;
-  ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
+  ThmDeps.enable ();
+  if isar then ml_prompts "ML> " "ML# "
+  else ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
   if isar then Isar.sync_main () else isa_restart ());