# HG changeset patch
# User wenzelm
# Date 952373316 -3600
# Node ID 611342539639667f16b5fe111e8818a2e8941612
# Parent  ebbbfdb35c848eb84f887896a34f5c52a3118125
moved use_mltext, use_mltext_theory, use_let, use_setup to context.ML;

diff -r ebbbfdb35c84 -r 611342539639 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon Mar 06 21:08:15 2000 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Mar 06 21:08:36 2000 +0100
@@ -104,11 +104,11 @@
   Context.setmp (try Toplevel.theory_of state) ThyInfo.use name);
 
 (*passes changes of theory context*)
-val use_mltext_theory = Toplevel.theory' o IsarThy.use_mltext_theory;
+val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory;
 
 (*ignore result theory context*)
 fun use_mltext v txt = Toplevel.keep' (fn verb => fn state =>
-  (IsarThy.use_mltext txt (v andalso verb) (try Toplevel.theory_of state)));
+  (Context.use_mltext txt (v andalso verb) (try Toplevel.theory_of state)));
 
 (*Note: commit is dynamically bound*)
 val use_commit = use_mltext false "commit();";
diff -r ebbbfdb35c84 -r 611342539639 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Mar 06 21:08:15 2000 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Mar 06 21:08:36 2000 +0100
@@ -223,7 +223,7 @@
 
 val setupP =
   OuterSyntax.command "setup" "apply ML theory setup" K.thy_decl
-    (P.text >> (Toplevel.theory o IsarThy.use_setup));
+    (P.text >> (Toplevel.theory o Context.use_setup));
 
 
 (* translation functions *)
diff -r ebbbfdb35c84 -r 611342539639 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Mon Mar 06 21:08:15 2000 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Mon Mar 06 21:08:36 2000 +0100
@@ -141,9 +141,6 @@
     -> Toplevel.transition -> Toplevel.transition
   val finally_i: (thm list * Comment.interest) option * Comment.text
     -> Toplevel.transition -> Toplevel.transition
-  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
   val print_translation: string -> theory -> theory
@@ -456,51 +453,37 @@
 end;
 
 
-(* use ML text *)
-
-fun use_mltext txt verb opt_thy = Context.setmp opt_thy (use_text writeln verb) txt;
-fun use_mltext_theory txt verb thy = #2 (Context.pass_theory thy (use_text writeln verb) 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");
-
-val use_setup =
-  use_let "setup: (theory -> theory) list" "Library.apply setup";
-
-
 (* translation functions *)
 
 val parse_ast_translation =
-  use_let "parse_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
+  Context.use_let "parse_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
     "Theory.add_trfuns (parse_ast_translation, [], [], [])";
 
 val parse_translation =
-  use_let "parse_translation: (string * (term list -> term)) list"
+  Context.use_let "parse_translation: (string * (term list -> term)) list"
     "Theory.add_trfuns ([], parse_translation, [], [])";
 
 val print_translation =
-  use_let "print_translation: (string * (term list -> term)) list"
+  Context.use_let "print_translation: (string * (term list -> term)) list"
     "Theory.add_trfuns ([], [], print_translation, [])";
 
 val print_ast_translation =
-  use_let "print_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
+  Context.use_let "print_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
     "Theory.add_trfuns ([], [], [], print_ast_translation)";
 
 val typed_print_translation =
-  use_let "typed_print_translation: (string * (bool -> typ -> term list -> term)) list"
+  Context.use_let "typed_print_translation: (string * (bool -> typ -> term list -> term)) list"
     "Theory.add_trfunsT typed_print_translation";
 
 val token_translation =
-  use_let "token_translation: (string * string * (string -> string * int)) list"
+  Context.use_let "token_translation: (string * string * (string -> string * int)) list"
     "Theory.add_tokentrfuns token_translation";
 
 
 (* add_oracle *)
 
 fun add_oracle ((name, txt), comment_ignore) =
-  use_let
+  Context.use_let
     "oracle: bstring * (Sign.sg * Object.T -> term)"
     "Theory.add_oracle oracle"
     ("(" ^ quote name ^ ", " ^ txt ^ ")");