# HG changeset patch
# User wenzelm
# Date 938357043 -7200
# Node ID 88392b7bc54937f54e9e4844445229ab483955bd
# Parent  fe818734c387ec3a0a0f9b58c5aaf300c7693384
use_mltext: Context.setmp only;
use_mltext(_theory): verbose if int;

diff -r fe818734c387 -r 88392b7bc549 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Sun Sep 26 16:42:14 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Sun Sep 26 16:44:03 1999 +0200
@@ -135,8 +135,8 @@
     -> Toplevel.transition -> Toplevel.transition
   val finally_i: (thm list * Comment.interest) option * Comment.text
     -> Toplevel.transition -> Toplevel.transition
-  val use_mltext: string -> theory option -> theory option
-  val use_mltext_theory: string -> theory -> theory
+  val use_mltext: string -> bool -> theory option -> unit
+  val use_mltext_theory: string -> bool -> theory -> theory
   val use_setup: string -> theory -> theory
   val parse_ast_translation: string -> theory -> theory
   val parse_translation: string -> theory -> theory
@@ -431,10 +431,10 @@
 
 (* use ML text *)
 
-fun use_mltext txt opt_thy = #2 (Context.pass opt_thy (use_text false) txt);
-fun use_mltext_theory txt thy = #2 (Context.pass_theory thy (use_text false) txt);
+fun use_mltext txt verb opt_thy = Context.setmp opt_thy (use_text verb) txt;
+fun use_mltext_theory txt verb thy = #2 (Context.pass_theory thy (use_text verb) txt);
 
-fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");");
+fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;
 
 fun use_let name body txt =
   use_context ("let val " ^ name ^ " = " ^ txt ^ " in\n" ^ body ^ " end");