--- a/src/Doc/Codegen/Setup.thy Fri Mar 21 08:13:23 2014 +0100
+++ b/src/Doc/Codegen/Setup.thy Fri Mar 21 10:45:03 2014 +0100
@@ -19,10 +19,10 @@
let
val typ = Simple_Syntax.read_typ;
in
- Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
+ Sign.del_modesyntax (Symbol.xsymbolsN, false)
[("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
- Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
+ Sign.add_modesyntax (Symbol.xsymbolsN, false)
[("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
end
--- a/src/HOL/HOLCF/Tools/cont_consts.ML Fri Mar 21 08:13:23 2014 +0100
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML Fri Mar 21 10:45:03 2014 +0100
@@ -80,7 +80,7 @@
val transformed_decls = map (transform thy) contconst_decls
in
thy
- |> Sign.add_consts_i (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls)
+ |> Sign.add_consts (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls)
|> Sign.add_trrules (maps #3 transformed_decls)
end
--- a/src/HOL/Imperative_HOL/Overview.thy Fri Mar 21 08:13:23 2014 +0100
+++ b/src/HOL/Imperative_HOL/Overview.thy Fri Mar 21 10:45:03 2014 +0100
@@ -12,10 +12,10 @@
let
val typ = Simple_Syntax.read_typ;
in
- Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
+ Sign.del_modesyntax (Symbol.xsymbolsN, false)
[("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
- Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
+ Sign.add_modesyntax (Symbol.xsymbolsN, false)
[("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
end
--- a/src/HOL/Import/import_rule.ML Fri Mar 21 08:13:23 2014 +0100
+++ b/src/HOL/Import/import_rule.ML Fri Mar 21 10:45:03 2014 +0100
@@ -172,7 +172,7 @@
let
val rhs = term_of rhs
val typ = type_of rhs
- val thy1 = Sign.add_consts_i [(Binding.name constname, typ, NoSyn)] thy
+ val thy1 = Sign.add_consts [(Binding.name constname, typ, NoSyn)] thy
val eq = Logic.mk_equals (Const (Sign.intern_const thy1 constname, typ), rhs)
val (thms, thy2) = Global_Theory.add_defs false
[((Binding.suffix_name "_hldef" (Binding.name constname), eq), [])] thy1
--- a/src/HOL/Library/bnf_decl.ML Fri Mar 21 08:13:23 2014 +0100
+++ b/src/HOL/Library/bnf_decl.ML Fri Mar 21 10:45:03 2014 +0100
@@ -57,7 +57,7 @@
(if nwits = 1 then [0] else 1 upto nwits);
val lthy = Local_Theory.background_theory
- (Sign.add_consts_i ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) ::
+ (Sign.add_consts ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) ::
map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @
map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs))
lthy;
--- a/src/HOL/Nominal/nominal_datatype.ML Fri Mar 21 08:13:23 2014 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Mar 21 10:45:03 2014 +0100
@@ -761,7 +761,7 @@
(Const (rep_name, T --> T') $ lhs, rhs));
val def_name = (Long_Name.base_name cname) ^ "_def";
val ([def_thm], thy') = thy |>
- Sign.add_consts_i [(cname', constrT, mx)] |>
+ Sign.add_consts [(cname', constrT, mx)] |>
(Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)];
in (thy', defs @ [def_thm], eqns @ [eqn]) end;
@@ -1993,7 +1993,7 @@
val (reccomb_defs, thy12) =
thy11
- |> Sign.add_consts_i (map (fn ((name, T), T') =>
+ |> Sign.add_consts (map (fn ((name, T), T') =>
(Binding.name (Long_Name.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
(reccomb_names ~~ recTs ~~ rec_result_Ts))
|> (Global_Theory.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Fri Mar 21 08:13:23 2014 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Fri Mar 21 10:45:03 2014 +0100
@@ -1001,7 +1001,7 @@
in
(c,
((Symtab.update (s, (c, ty)) tab, Name.declare s ctxt),
- Sign.add_consts_i [(b, T, NoSyn)] thy))
+ Sign.add_consts [(b, T, NoSyn)] thy))
end;
fun add_def prfx types pfuns consts (id, (s, e)) (ids as (tab, ctxt), thy) =
--- a/src/HOL/Tools/Datatype/datatype.ML Fri Mar 21 08:13:23 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Fri Mar 21 10:45:03 2014 +0100
@@ -237,7 +237,7 @@
HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (Rep_name, T --> Univ_elT) $ lhs, rhs));
val ([def_thm], thy') =
thy
- |> Sign.add_consts_i [(cname', constrT, mx)]
+ |> Sign.add_consts [(cname', constrT, mx)]
|> (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)];
in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
@@ -262,7 +262,7 @@
val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) =
fold dt_constr_defs
(hd descr ~~ new_type_names ~~ map #2 typedefs ~~ newTs ~~ constr_syntax)
- (thy3 |> Sign.add_consts_i iso_decls |> Sign.parent_path, [], [], [], []);
+ (thy3 |> Sign.add_consts iso_decls |> Sign.parent_path, [], [], [], []);
(*********** isomorphisms for new types (introduced by typedef) ***********)
--- a/src/HOL/Tools/Datatype/rep_datatype.ML Fri Mar 21 08:13:23 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Fri Mar 21 10:45:03 2014 +0100
@@ -226,7 +226,7 @@
val (reccomb_defs, thy2) =
thy1
- |> Sign.add_consts_i (map (fn ((name, T), T') =>
+ |> Sign.add_consts (map (fn ((name, T), T') =>
(Binding.name (Long_Name.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn))
(reccomb_names ~~ recTs ~~ rec_result_Ts))
|> (Global_Theory.add_defs false o map Thm.no_attributes)
--- a/src/HOL/Tools/Function/size.ML Fri Mar 21 08:13:23 2014 +0100
+++ b/src/HOL/Tools/Function/size.ML Fri Mar 21 10:45:03 2014 +0100
@@ -134,7 +134,7 @@
val ((size_def_thms, size_def_thms'), thy') =
thy
- |> Sign.add_consts_i (map (fn (s, T) =>
+ |> Sign.add_consts (map (fn (s, T) =>
(Binding.name (Long_Name.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
(size_names ~~ recTs1))
|> Global_Theory.add_defs false
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Mar 21 08:13:23 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Mar 21 10:45:03 2014 +0100
@@ -1212,7 +1212,7 @@
val constname = "quickcheck"
val full_constname = Sign.full_bname thy constname
val constT = map snd vs' ---> @{typ bool}
- val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
+ val thy1 = Sign.add_consts [(Binding.name constname, constT, NoSyn)] thy
val const = Const (full_constname, constT)
val t =
Logic.list_implies
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Mar 21 08:13:23 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Mar 21 10:45:03 2014 +0100
@@ -1146,7 +1146,7 @@
val lhs = Const (mode_cname, funT)
val def = Logic.mk_equals (lhs, predterm)
val ([definition], thy') = thy |>
- Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
+ Sign.add_consts [(Binding.name mode_cbasename, funT, NoSyn)] |>
Global_Theory.add_defs false [((Binding.name (Thm.def_name mode_cbasename), def), [])]
val ctxt' = Proof_Context.init_global thy'
val rules as ((intro, elim), _) =
@@ -1171,7 +1171,7 @@
val mode_cname = create_constname_of_mode options thy function_name_prefix name T mode
val funT = Comp_Mod.funT_of comp_modifiers mode T
in
- thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
+ thy |> Sign.add_consts [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
|> set_function_name (Comp_Mod.compilation comp_modifiers) name mode mode_cname
end;
in
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Mar 21 08:13:23 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Mar 21 10:45:03 2014 +0100
@@ -284,7 +284,7 @@
end
val intr_tss = map mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss))
val (intrs, thy') = thy
- |> Sign.add_consts_i
+ |> Sign.add_consts
(map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn))
dst_preds)
|> fold_map Specification.axiom (* FIXME !?!?!?! *)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Mar 21 08:13:23 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Mar 21 10:45:03 2014 +0100
@@ -87,7 +87,7 @@
val lhs = list_comb (Const (full_constname, constT), params @ args)
val def = Logic.mk_equals (lhs, atom)
val ([definition], thy') = thy
- |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
+ |> Sign.add_consts [(Binding.name constname, constT, NoSyn)]
|> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])]
in
(lhs, ((full_constname, [definition]) :: defs, thy'))
@@ -119,7 +119,7 @@
Logic.mk_equals (fold Envir.expand_term_frees (map single subst) lhs, rhs)
val new_defs = map mk_def srs
val (definition, thy') = thy
- |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
+ |> Sign.add_consts [(Binding.name constname, constT, NoSyn)]
|> fold_map Specification.axiom (* FIXME !?!?!?! *)
(map_index (fn (i, t) =>
((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs)
@@ -245,7 +245,7 @@
val lhs = list_comb (const, frees)
val def = Logic.mk_equals (lhs, abs_arg')
val ([definition], thy') = thy
- |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
+ |> Sign.add_consts [(Binding.name constname, constT, NoSyn)]
|> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])]
in
(list_comb (Logic.varify_global const, vars),
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Fri Mar 21 08:13:23 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Fri Mar 21 10:45:03 2014 +0100
@@ -94,7 +94,7 @@
end handle Pattern.Unif => NONE)
val specialised_intros_t = map_filter I (map specialise_intro intros)
val thy' =
- Sign.add_consts_i [(Binding.name (Long_Name.base_name constname), constT, NoSyn)] thy
+ Sign.add_consts [(Binding.name (Long_Name.base_name constname), constT, NoSyn)] thy
val specialised_intros = map (Skip_Proof.make_thm thy') specialised_intros_t
val exported_intros = Variable.exportT ctxt' ctxt specialised_intros
val [t, specialised_t] = Variable.exportT_terms ctxt' ctxt
--- a/src/Pure/Isar/isar_syn.ML Fri Mar 21 08:13:23 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML Fri Mar 21 10:45:03 2014 +0100
@@ -108,7 +108,7 @@
val _ =
Outer_Syntax.command @{command_spec "consts"} "declare constants"
- (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts));
+ (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd));
val mode_spec =
(@{keyword "output"} >> K ("", false)) ||
@@ -119,11 +119,13 @@
val _ =
Outer_Syntax.command @{command_spec "syntax"} "add raw syntax clauses"
- (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_modesyntax));
+ (opt_mode -- Scan.repeat1 Parse.const_decl
+ >> (Toplevel.theory o uncurry Sign.add_modesyntax_cmd));
val _ =
Outer_Syntax.command @{command_spec "no_syntax"} "delete raw syntax clauses"
- (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_modesyntax));
+ (opt_mode -- Scan.repeat1 Parse.const_decl
+ >> (Toplevel.theory o uncurry Sign.del_modesyntax_cmd));
(* translations *)
--- a/src/Pure/Isar/object_logic.ML Fri Mar 21 08:13:23 2014 +0100
+++ b/src/Pure/Isar/object_logic.ML Fri Mar 21 10:45:03 2014 +0100
@@ -97,8 +97,8 @@
in
-val add_judgment = gen_add_judgment Sign.add_consts_i;
-val add_judgment_cmd = gen_add_judgment Sign.add_consts;
+val add_judgment = gen_add_judgment Sign.add_consts;
+val add_judgment_cmd = gen_add_judgment Sign.add_consts_cmd;
end;
--- a/src/Pure/Proof/extraction.ML Fri Mar 21 08:13:23 2014 +0100
+++ b/src/Pure/Proof/extraction.ML Fri Mar 21 10:45:03 2014 +0100
@@ -37,7 +37,7 @@
val add_syntax =
Sign.root_path
#> Sign.add_types_global [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)]
- #> Sign.add_consts_i
+ #> Sign.add_consts
[(Binding.name "typeof", typ "'b => Type", NoSyn),
(Binding.name "Type", typ "'a itself => Type", NoSyn),
(Binding.name "Null", typ "Null", NoSyn),
@@ -791,7 +791,7 @@
val fu = Type.legacy_freeze u;
val (def_thms, thy') = if t = nullt then ([], thy) else
thy
- |> Sign.add_consts_i [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
+ |> Sign.add_consts [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
|> Global_Theory.add_defs false
[((Binding.qualified_name (Thm.def_name (extr_name s vs)),
Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
--- a/src/Pure/Proof/proof_syntax.ML Fri Mar 21 08:13:23 2014 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Fri Mar 21 10:45:03 2014 +0100
@@ -35,7 +35,7 @@
fun add_proof_atom_consts names thy =
thy
|> Sign.root_path
- |> Sign.add_consts_i (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names);
+ |> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names);
(** constants for application and abstraction **)
@@ -54,7 +54,7 @@
((Binding.name "OfClass", (Term.a_itselfT --> propT) --> proofT), NoSyn),
((Binding.name "MinProof", proofT), Delimfix "?")]
|> Sign.add_nonterminals_global [Binding.name "param", Binding.name "params"]
- |> Sign.add_syntax_i
+ |> Sign.add_syntax
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
@@ -62,7 +62,7 @@
("", paramT --> paramT, Delimfix "'(_')"),
("", idtT --> paramsT, Delimfix "_"),
("", paramT --> paramsT, Delimfix "_")]
- |> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
+ |> Sign.add_modesyntax (Symbol.xsymbolsN, true)
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
(Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
(Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \<bullet>/ _)", [4, 5], 4))]
--- a/src/Pure/pure_thy.ML Fri Mar 21 08:13:23 2014 +0100
+++ b/src/Pure/pure_thy.ML Fri Mar 21 10:45:03 2014 +0100
@@ -49,8 +49,8 @@
val old_appl_syntax_setup =
Old_Appl_Syntax.put true #>
- Sign.del_modesyntax_i Syntax.mode_default applC_syntax #>
- Sign.add_syntax_i appl_syntax;
+ Sign.del_modesyntax Syntax.mode_default applC_syntax #>
+ Sign.add_syntax appl_syntax;
(* main content *)
@@ -75,8 +75,8 @@
"tvar_position", "id_position", "longid_position", "var_position",
"str_position", "string_position", "cartouche_position", "type_name",
"class_name"]))
- #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) token_markers)
- #> Sign.add_syntax_i
+ #> Sign.add_syntax (map (fn x => (x, typ "'a", NoSyn)) token_markers)
+ #> Sign.add_syntax
[("", typ "prop' => prop", Delimfix "_"),
("", typ "logic => any", Delimfix "_"),
("", typ "prop' => any", Delimfix "_"),
@@ -174,8 +174,8 @@
("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
(const "Pure.term", typ "logic => prop", Delimfix "TERM _"),
(const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
- #> Sign.add_syntax_i applC_syntax
- #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
+ #> Sign.add_syntax applC_syntax
+ #> Sign.add_modesyntax (Symbol.xsymbolsN, true)
[(tycon "fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
("_ofsort", typ "tid_position => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
@@ -190,11 +190,11 @@
("_DDDOT", typ "aprop", Delimfix "\\<dots>"),
("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
("_DDDOT", typ "logic", Delimfix "\\<dots>")]
- #> Sign.add_modesyntax_i ("", false)
+ #> Sign.add_modesyntax ("", false)
[(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))]
- #> Sign.add_modesyntax_i ("HTML", false)
+ #> Sign.add_modesyntax ("HTML", false)
[("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
- #> Sign.add_consts_i
+ #> Sign.add_consts
[(Binding.name "==", typ "'a => 'a => prop", Infix ("==", 2)),
(Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
(Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
@@ -209,7 +209,7 @@
#> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
#> Sign.parse_translation Syntax_Trans.pure_parse_translation
#> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
- #> Sign.add_consts_i
+ #> Sign.add_consts
[(qualify (Binding.name "term"), typ "'a => prop", NoSyn),
(qualify (Binding.name "sort_constraint"), typ "'a itself => prop", NoSyn),
(qualify (Binding.name "conjunction"), typ "prop => prop => prop", NoSyn)]
--- a/src/Pure/sign.ML Fri Mar 21 08:13:23 2014 +0100
+++ b/src/Pure/sign.ML Fri Mar 21 10:45:03 2014 +0100
@@ -73,18 +73,18 @@
val add_nonterminals: Proof.context -> binding list -> theory -> theory
val add_nonterminals_global: binding list -> theory -> theory
val add_type_abbrev: Proof.context -> binding * string list * typ -> theory -> theory
- val add_syntax: (string * string * mixfix) list -> theory -> theory
- val add_syntax_i: (string * typ * mixfix) list -> theory -> theory
- val add_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
- val add_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
- val del_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
- val del_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
+ val add_syntax: (string * typ * mixfix) list -> theory -> theory
+ val add_syntax_cmd: (string * string * mixfix) list -> theory -> theory
+ val add_modesyntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
+ val add_modesyntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
+ val del_modesyntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
+ val del_modesyntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
val declare_const: Proof.context -> (binding * typ) * mixfix -> theory -> term * theory
val declare_const_global: (binding * typ) * mixfix -> theory -> term * theory
- val add_consts: (binding * string * mixfix) list -> theory -> theory
- val add_consts_i: (binding * typ * mixfix) list -> theory -> theory
+ val add_consts: (binding * typ * mixfix) list -> theory -> theory
+ val add_consts_cmd: (binding * string * mixfix) list -> theory -> theory
val add_abbrev: string -> binding * term -> theory -> (term * term) * theory
val revert_abbrev: string -> string -> theory -> theory
val add_const_constraint: string * typ option -> theory -> theory
@@ -375,12 +375,12 @@
fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x;
-val add_modesyntax = gen_add_syntax Syntax.read_typ;
-val add_modesyntax_i = gen_add_syntax (K I);
+val add_modesyntax = gen_add_syntax (K I);
+val add_modesyntax_cmd = gen_add_syntax Syntax.read_typ;
val add_syntax = add_modesyntax Syntax.mode_default;
-val add_syntax_i = add_modesyntax_i Syntax.mode_default;
-val del_modesyntax = gen_syntax (Syntax.update_const_gram false) Syntax.read_typ;
-val del_modesyntax_i = gen_syntax (Syntax.update_const_gram false) (K I);
+val add_syntax_cmd = add_modesyntax_cmd Syntax.mode_default;
+val del_modesyntax = gen_syntax (Syntax.update_const_gram false) (K I);
+val del_modesyntax_cmd = gen_syntax (Syntax.update_const_gram false) Syntax.read_typ;
fun type_notation add mode args =
let
@@ -417,17 +417,17 @@
in
thy
|> map_consts (fold (Consts.declare (inherit_naming thy ctxt) o #1) args)
- |> add_syntax_i (map #2 args)
+ |> add_syntax (map #2 args)
|> pair (map #3 args)
end;
in
fun add_consts args thy =
- #2 (gen_add_consts Syntax.read_typ (Proof_Context.init_global thy) args thy);
+ #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy);
-fun add_consts_i args thy =
- #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy);
+fun add_consts_cmd args thy =
+ #2 (gen_add_consts Syntax.read_typ (Proof_Context.init_global thy) args thy);
fun declare_const ctxt ((b, T), mx) = yield_singleton (gen_add_consts (K I) ctxt) (b, T, mx);
fun declare_const_global arg thy = declare_const (Proof_Context.init_global thy) arg thy;
@@ -468,7 +468,7 @@
|> map_sign (fn (syn, tsig, consts) =>
let val tsig' = Type.add_class (Context.Theory thy) (bclass, classes) tsig;
in (syn, tsig', consts) end)
- |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
+ |> add_consts [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
fun primitive_classrel arg thy =
thy |> map_tsig (Type.add_classrel (Context.pretty_global thy) arg);
--- a/src/ZF/Tools/datatype_package.ML Fri Mar 21 08:13:23 2014 +0100
+++ b/src/ZF/Tools/datatype_package.ML Fri Mar 21 10:45:03 2014 +0100
@@ -244,21 +244,20 @@
fun add_recursor thy =
if need_recursor then
thy
- |> Sign.add_consts_i
- [(Binding.name recursor_base_name, recursor_typ, NoSyn)]
+ |> Sign.add_consts [(Binding.name recursor_base_name, recursor_typ, NoSyn)]
|> (snd o Global_Theory.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
else thy;
val (con_defs, thy0) = thy_path
- |> Sign.add_consts_i
- (map (fn (c, T, mx) => (Binding.name c, T, mx))
- ((case_base_name, case_typ, NoSyn) :: map #1 (flat con_ty_lists)))
- |> Global_Theory.add_defs false
- (map (Thm.no_attributes o apfst Binding.name)
- (case_def ::
- flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists))))
- ||> add_recursor
- ||> Sign.parent_path
+ |> Sign.add_consts
+ (map (fn (c, T, mx) => (Binding.name c, T, mx))
+ ((case_base_name, case_typ, NoSyn) :: map #1 (flat con_ty_lists)))
+ |> Global_Theory.add_defs false
+ (map (Thm.no_attributes o apfst Binding.name)
+ (case_def ::
+ flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists))))
+ ||> add_recursor
+ ||> Sign.parent_path;
val intr_names = map (Binding.name o #2) (flat con_ty_lists);
val (thy1, ind_result) =