# HG changeset patch # User wenzelm # Date 1395395103 -3600 # Node ID 17df7145a871044e3467ff1aea5e7dd7f63f9dc4 # Parent 69a9dfe71aed821d1c67debe08ef6d6e31fb71ab tuned signature; diff -r 69a9dfe71aed -r 17df7145a871 src/Doc/Codegen/Setup.thy --- 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 ("_\_", [4, 0], 3)), ("_constrain", typ "prop' => type => prop'", Mixfix ("_\_", [4, 0], 3))] #> - Sign.add_modesyntax_i (Symbol.xsymbolsN, false) + Sign.add_modesyntax (Symbol.xsymbolsN, false) [("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \ _", [4, 0], 3))] end diff -r 69a9dfe71aed -r 17df7145a871 src/HOL/HOLCF/Tools/cont_consts.ML --- 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 diff -r 69a9dfe71aed -r 17df7145a871 src/HOL/Imperative_HOL/Overview.thy --- 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 ("_\_", [4, 0], 3)), ("_constrain", typ "prop' => type => prop'", Mixfix ("_\_", [4, 0], 3))] #> - Sign.add_modesyntax_i (Symbol.xsymbolsN, false) + Sign.add_modesyntax (Symbol.xsymbolsN, false) [("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \ _", [4, 0], 3))] end diff -r 69a9dfe71aed -r 17df7145a871 src/HOL/Import/import_rule.ML --- 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 diff -r 69a9dfe71aed -r 17df7145a871 src/HOL/Library/bnf_decl.ML --- 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; diff -r 69a9dfe71aed -r 17df7145a871 src/HOL/Nominal/nominal_datatype.ML --- 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') => diff -r 69a9dfe71aed -r 17df7145a871 src/HOL/SPARK/Tools/spark_vcs.ML --- 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) = diff -r 69a9dfe71aed -r 17df7145a871 src/HOL/Tools/Datatype/datatype.ML --- 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) ***********) diff -r 69a9dfe71aed -r 17df7145a871 src/HOL/Tools/Datatype/rep_datatype.ML --- 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) diff -r 69a9dfe71aed -r 17df7145a871 src/HOL/Tools/Function/size.ML --- 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 diff -r 69a9dfe71aed -r 17df7145a871 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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 diff -r 69a9dfe71aed -r 17df7145a871 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 diff -r 69a9dfe71aed -r 17df7145a871 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- 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 !?!?!?! *) diff -r 69a9dfe71aed -r 17df7145a871 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- 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), diff -r 69a9dfe71aed -r 17df7145a871 src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML --- 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 diff -r 69a9dfe71aed -r 17df7145a871 src/Pure/Isar/isar_syn.ML --- 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 *) diff -r 69a9dfe71aed -r 17df7145a871 src/Pure/Isar/object_logic.ML --- 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; diff -r 69a9dfe71aed -r 17df7145a871 src/Pure/Proof/extraction.ML --- 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)), [])] diff -r 69a9dfe71aed -r 17df7145a871 src/Pure/Proof/proof_syntax.ML --- 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>\_./ _)", [0, 3], 3)), (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \/ _)", [4, 5], 4)), (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \/ _)", [4, 5], 4))] diff -r 69a9dfe71aed -r 17df7145a871 src/Pure/pure_thy.ML --- 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 ("(_/ \\ _)", [1, 0], 0)), ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\ _)", [0, 0], 0)), ("_ofsort", typ "tid_position => sort => type", Mixfix ("_\\_", [1000, 0], 1000)), @@ -190,11 +190,11 @@ ("_DDDOT", typ "aprop", Delimfix "\\"), ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\_\\)/ \\ _)", [0, 1], 1)), ("_DDDOT", typ "logic", Delimfix "\\")] - #> 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\\_./ _)", [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)] diff -r 69a9dfe71aed -r 17df7145a871 src/Pure/sign.ML --- 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); diff -r 69a9dfe71aed -r 17df7145a871 src/ZF/Tools/datatype_package.ML --- 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) =