src/Pure/Isar/isar_thy.ML
changeset 7614 88392b7bc549
parent 7590 76c9e71d491a
child 7633 838077e40a46
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Sun Sep 26 16:42:14 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Sun Sep 26 16:44:03 1999 +0200
     1.3 @@ -135,8 +135,8 @@
     1.4      -> Toplevel.transition -> Toplevel.transition
     1.5    val finally_i: (thm list * Comment.interest) option * Comment.text
     1.6      -> Toplevel.transition -> Toplevel.transition
     1.7 -  val use_mltext: string -> theory option -> theory option
     1.8 -  val use_mltext_theory: string -> theory -> theory
     1.9 +  val use_mltext: string -> bool -> theory option -> unit
    1.10 +  val use_mltext_theory: string -> bool -> theory -> theory
    1.11    val use_setup: string -> theory -> theory
    1.12    val parse_ast_translation: string -> theory -> theory
    1.13    val parse_translation: string -> theory -> theory
    1.14 @@ -431,10 +431,10 @@
    1.15  
    1.16  (* use ML text *)
    1.17  
    1.18 -fun use_mltext txt opt_thy = #2 (Context.pass opt_thy (use_text false) txt);
    1.19 -fun use_mltext_theory txt thy = #2 (Context.pass_theory thy (use_text false) txt);
    1.20 +fun use_mltext txt verb opt_thy = Context.setmp opt_thy (use_text verb) txt;
    1.21 +fun use_mltext_theory txt verb thy = #2 (Context.pass_theory thy (use_text verb) txt);
    1.22  
    1.23 -fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");");
    1.24 +fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;
    1.25  
    1.26  fun use_let name body txt =
    1.27    use_context ("let val " ^ name ^ " = " ^ txt ^ " in\n" ^ body ^ " end");