--- a/src/Pure/Isar/isar_cmd.ML Tue Nov 11 21:14:19 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Wed Nov 12 10:30:59 2014 +0100
@@ -60,14 +60,14 @@
fun global_setup source =
ML_Lex.read_source false source
- |> ML_Context.expression (#range source)
- "val setup: theory -> theory" "Context.map_theory setup"
+ |> ML_Context.expression (#range source) "setup" "theory -> theory"
+ "Context.map_theory setup"
|> Context.theory_map;
fun local_setup source =
ML_Lex.read_source false source
- |> ML_Context.expression (#range source)
- "val local_setup: local_theory -> local_theory" "Context.map_proof local_setup"
+ |> ML_Context.expression (#range source) "local_setup" "local_theory -> local_theory"
+ "Context.map_proof local_setup"
|> Context.proof_map;
@@ -75,36 +75,36 @@
fun parse_ast_translation source =
ML_Lex.read_source false source
- |> ML_Context.expression (#range source)
- "val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
+ |> ML_Context.expression (#range source) "parse_ast_translation"
+ "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
"Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
|> Context.theory_map;
fun parse_translation source =
ML_Lex.read_source false source
- |> ML_Context.expression (#range source)
- "val parse_translation: (string * (Proof.context -> term list -> term)) list"
+ |> ML_Context.expression (#range source) "parse_translation"
+ "(string * (Proof.context -> term list -> term)) list"
"Context.map_theory (Sign.parse_translation parse_translation)"
|> Context.theory_map;
fun print_translation source =
ML_Lex.read_source false source
- |> ML_Context.expression (#range source)
- "val print_translation: (string * (Proof.context -> term list -> term)) list"
+ |> ML_Context.expression (#range source) "print_translation"
+ "(string * (Proof.context -> term list -> term)) list"
"Context.map_theory (Sign.print_translation print_translation)"
|> Context.theory_map;
fun typed_print_translation source =
ML_Lex.read_source false source
- |> ML_Context.expression (#range source)
- "val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list"
+ |> ML_Context.expression (#range source) "typed_print_translation"
+ "(string * (Proof.context -> typ -> term list -> term)) list"
"Context.map_theory (Sign.typed_print_translation typed_print_translation)"
|> Context.theory_map;
fun print_ast_translation source =
ML_Lex.read_source false source
- |> ML_Context.expression (#range source)
- "val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
+ |> ML_Context.expression (#range source) "print_ast_translation"
+ "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
"Context.map_theory (Sign.print_ast_translation print_ast_translation)"
|> Context.theory_map;
@@ -160,8 +160,7 @@
fun declaration {syntax, pervasive} source =
ML_Lex.read_source false source
- |> ML_Context.expression (#range source)
- "val declaration: Morphism.declaration"
+ |> ML_Context.expression (#range source) "declaration" "Morphism.declaration"
("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
\pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
|> Context.proof_map;
@@ -171,8 +170,8 @@
fun simproc_setup name lhss source identifier =
ML_Lex.read_source false source
- |> ML_Context.expression (#range source)
- "val proc: Morphism.morphism -> Proof.context -> cterm -> thm option"
+ |> ML_Context.expression (#range source) "proc"
+ "Morphism.morphism -> Proof.context -> cterm -> thm option"
("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
\lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
\identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})")