src/Pure/Isar/isar_cmd.ML
changeset 58991 92b6f4e68c5a
parent 58979 162a4c2e97bc
child 59029 c907cbe36713
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Nov 11 21:14:19 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Nov 12 10:30:59 2014 +0100
     1.3 @@ -60,14 +60,14 @@
     1.4  
     1.5  fun global_setup source =
     1.6    ML_Lex.read_source false source
     1.7 -  |> ML_Context.expression (#range source)
     1.8 -    "val setup: theory -> theory" "Context.map_theory setup"
     1.9 +  |> ML_Context.expression (#range source) "setup" "theory -> theory"
    1.10 +    "Context.map_theory setup"
    1.11    |> Context.theory_map;
    1.12  
    1.13  fun local_setup source =
    1.14    ML_Lex.read_source false source
    1.15 -  |> ML_Context.expression (#range source)
    1.16 -    "val local_setup: local_theory -> local_theory" "Context.map_proof local_setup"
    1.17 +  |> ML_Context.expression (#range source) "local_setup" "local_theory -> local_theory"
    1.18 +    "Context.map_proof local_setup"
    1.19    |> Context.proof_map;
    1.20  
    1.21  
    1.22 @@ -75,36 +75,36 @@
    1.23  
    1.24  fun parse_ast_translation source =
    1.25    ML_Lex.read_source false source
    1.26 -  |> ML_Context.expression (#range source)
    1.27 -    "val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    1.28 +  |> ML_Context.expression (#range source) "parse_ast_translation"
    1.29 +    "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    1.30      "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
    1.31    |> Context.theory_map;
    1.32  
    1.33  fun parse_translation source =
    1.34    ML_Lex.read_source false source
    1.35 -  |> ML_Context.expression (#range source)
    1.36 -    "val parse_translation: (string * (Proof.context -> term list -> term)) list"
    1.37 +  |> ML_Context.expression (#range source) "parse_translation"
    1.38 +    "(string * (Proof.context -> term list -> term)) list"
    1.39      "Context.map_theory (Sign.parse_translation parse_translation)"
    1.40    |> Context.theory_map;
    1.41  
    1.42  fun print_translation source =
    1.43    ML_Lex.read_source false source
    1.44 -  |> ML_Context.expression (#range source)
    1.45 -    "val print_translation: (string * (Proof.context -> term list -> term)) list"
    1.46 +  |> ML_Context.expression (#range source) "print_translation"
    1.47 +    "(string * (Proof.context -> term list -> term)) list"
    1.48      "Context.map_theory (Sign.print_translation print_translation)"
    1.49    |> Context.theory_map;
    1.50  
    1.51  fun typed_print_translation source =
    1.52    ML_Lex.read_source false source
    1.53 -  |> ML_Context.expression (#range source)
    1.54 -    "val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list"
    1.55 +  |> ML_Context.expression (#range source) "typed_print_translation"
    1.56 +    "(string * (Proof.context -> typ -> term list -> term)) list"
    1.57      "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
    1.58    |> Context.theory_map;
    1.59  
    1.60  fun print_ast_translation source =
    1.61    ML_Lex.read_source false source
    1.62 -  |> ML_Context.expression (#range source)
    1.63 -    "val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    1.64 +  |> ML_Context.expression (#range source) "print_ast_translation"
    1.65 +    "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    1.66      "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
    1.67    |> Context.theory_map;
    1.68  
    1.69 @@ -160,8 +160,7 @@
    1.70  
    1.71  fun declaration {syntax, pervasive} source =
    1.72    ML_Lex.read_source false source
    1.73 -  |> ML_Context.expression (#range source)
    1.74 -    "val declaration: Morphism.declaration"
    1.75 +  |> ML_Context.expression (#range source) "declaration" "Morphism.declaration"
    1.76      ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
    1.77        \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
    1.78    |> Context.proof_map;
    1.79 @@ -171,8 +170,8 @@
    1.80  
    1.81  fun simproc_setup name lhss source identifier =
    1.82    ML_Lex.read_source false source
    1.83 -  |> ML_Context.expression (#range source)
    1.84 -    "val proc: Morphism.morphism -> Proof.context -> cterm -> thm option"
    1.85 +  |> ML_Context.expression (#range source) "proc"
    1.86 +    "Morphism.morphism -> Proof.context -> cterm -> thm option"
    1.87      ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
    1.88        \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
    1.89        \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})")