src/Pure/Isar/isar_thy.ML
changeset 8349 611342539639
parent 8236 df3f983f5858
child 8371 7313627803f4
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Mon Mar 06 21:08:15 2000 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Mon Mar 06 21:08:36 2000 +0100
     1.3 @@ -141,9 +141,6 @@
     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 -> bool -> theory option -> unit
     1.8 -  val use_mltext_theory: string -> bool -> theory -> theory
     1.9 -  val use_setup: string -> theory -> theory
    1.10    val parse_ast_translation: string -> theory -> theory
    1.11    val parse_translation: string -> theory -> theory
    1.12    val print_translation: string -> theory -> theory
    1.13 @@ -456,51 +453,37 @@
    1.14  end;
    1.15  
    1.16  
    1.17 -(* use ML text *)
    1.18 -
    1.19 -fun use_mltext txt verb opt_thy = Context.setmp opt_thy (use_text writeln verb) txt;
    1.20 -fun use_mltext_theory txt verb thy = #2 (Context.pass_theory thy (use_text writeln verb) txt);
    1.21 -
    1.22 -fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;
    1.23 -
    1.24 -fun use_let name body txt =
    1.25 -  use_context ("let val " ^ name ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
    1.26 -
    1.27 -val use_setup =
    1.28 -  use_let "setup: (theory -> theory) list" "Library.apply setup";
    1.29 -
    1.30 -
    1.31  (* translation functions *)
    1.32  
    1.33  val parse_ast_translation =
    1.34 -  use_let "parse_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
    1.35 +  Context.use_let "parse_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
    1.36      "Theory.add_trfuns (parse_ast_translation, [], [], [])";
    1.37  
    1.38  val parse_translation =
    1.39 -  use_let "parse_translation: (string * (term list -> term)) list"
    1.40 +  Context.use_let "parse_translation: (string * (term list -> term)) list"
    1.41      "Theory.add_trfuns ([], parse_translation, [], [])";
    1.42  
    1.43  val print_translation =
    1.44 -  use_let "print_translation: (string * (term list -> term)) list"
    1.45 +  Context.use_let "print_translation: (string * (term list -> term)) list"
    1.46      "Theory.add_trfuns ([], [], print_translation, [])";
    1.47  
    1.48  val print_ast_translation =
    1.49 -  use_let "print_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
    1.50 +  Context.use_let "print_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
    1.51      "Theory.add_trfuns ([], [], [], print_ast_translation)";
    1.52  
    1.53  val typed_print_translation =
    1.54 -  use_let "typed_print_translation: (string * (bool -> typ -> term list -> term)) list"
    1.55 +  Context.use_let "typed_print_translation: (string * (bool -> typ -> term list -> term)) list"
    1.56      "Theory.add_trfunsT typed_print_translation";
    1.57  
    1.58  val token_translation =
    1.59 -  use_let "token_translation: (string * string * (string -> string * int)) list"
    1.60 +  Context.use_let "token_translation: (string * string * (string -> string * int)) list"
    1.61      "Theory.add_tokentrfuns token_translation";
    1.62  
    1.63  
    1.64  (* add_oracle *)
    1.65  
    1.66  fun add_oracle ((name, txt), comment_ignore) =
    1.67 -  use_let
    1.68 +  Context.use_let
    1.69      "oracle: bstring * (Sign.sg * Object.T -> term)"
    1.70      "Theory.add_oracle oracle"
    1.71      ("(" ^ quote name ^ ", " ^ txt ^ ")");