tuned signature;
authorwenzelm
Fri Mar 21 10:45:03 2014 +0100 (2014-03-21)
changeset 5623917df7145a871
parent 56237 69a9dfe71aed
child 56240 938c6c7e10eb
tuned signature;
src/Doc/Codegen/Setup.thy
src/HOL/HOLCF/Tools/cont_consts.ML
src/HOL/Imperative_HOL/Overview.thy
src/HOL/Import/import_rule.ML
src/HOL/Library/bnf_decl.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/SPARK/Tools/spark_vcs.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/rep_datatype.ML
src/HOL/Tools/Function/size.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/object_logic.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
src/ZF/Tools/datatype_package.ML
     1.1 --- a/src/Doc/Codegen/Setup.thy	Fri Mar 21 08:13:23 2014 +0100
     1.2 +++ b/src/Doc/Codegen/Setup.thy	Fri Mar 21 10:45:03 2014 +0100
     1.3 @@ -19,10 +19,10 @@
     1.4  let
     1.5    val typ = Simple_Syntax.read_typ;
     1.6  in
     1.7 -  Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
     1.8 +  Sign.del_modesyntax (Symbol.xsymbolsN, false)
     1.9     [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
    1.10      ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
    1.11 -  Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
    1.12 +  Sign.add_modesyntax (Symbol.xsymbolsN, false)
    1.13     [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
    1.14      ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
    1.15  end
     2.1 --- a/src/HOL/HOLCF/Tools/cont_consts.ML	Fri Mar 21 08:13:23 2014 +0100
     2.2 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML	Fri Mar 21 10:45:03 2014 +0100
     2.3 @@ -80,7 +80,7 @@
     2.4      val transformed_decls = map (transform thy) contconst_decls
     2.5    in
     2.6      thy
     2.7 -    |> Sign.add_consts_i (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls)
     2.8 +    |> Sign.add_consts (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls)
     2.9      |> Sign.add_trrules (maps #3 transformed_decls)
    2.10    end
    2.11  
     3.1 --- a/src/HOL/Imperative_HOL/Overview.thy	Fri Mar 21 08:13:23 2014 +0100
     3.2 +++ b/src/HOL/Imperative_HOL/Overview.thy	Fri Mar 21 10:45:03 2014 +0100
     3.3 @@ -12,10 +12,10 @@
     3.4  let
     3.5    val typ = Simple_Syntax.read_typ;
     3.6  in
     3.7 -  Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
     3.8 +  Sign.del_modesyntax (Symbol.xsymbolsN, false)
     3.9     [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
    3.10      ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
    3.11 -  Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
    3.12 +  Sign.add_modesyntax (Symbol.xsymbolsN, false)
    3.13     [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
    3.14      ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
    3.15  end
     4.1 --- a/src/HOL/Import/import_rule.ML	Fri Mar 21 08:13:23 2014 +0100
     4.2 +++ b/src/HOL/Import/import_rule.ML	Fri Mar 21 10:45:03 2014 +0100
     4.3 @@ -172,7 +172,7 @@
     4.4    let
     4.5      val rhs = term_of rhs
     4.6      val typ = type_of rhs
     4.7 -    val thy1 = Sign.add_consts_i [(Binding.name constname, typ, NoSyn)] thy
     4.8 +    val thy1 = Sign.add_consts [(Binding.name constname, typ, NoSyn)] thy
     4.9      val eq = Logic.mk_equals (Const (Sign.intern_const thy1 constname, typ), rhs)
    4.10      val (thms, thy2) = Global_Theory.add_defs false
    4.11        [((Binding.suffix_name "_hldef" (Binding.name constname), eq), [])] thy1
     5.1 --- a/src/HOL/Library/bnf_decl.ML	Fri Mar 21 08:13:23 2014 +0100
     5.2 +++ b/src/HOL/Library/bnf_decl.ML	Fri Mar 21 10:45:03 2014 +0100
     5.3 @@ -57,7 +57,7 @@
     5.4        (if nwits = 1 then [0] else 1 upto nwits);
     5.5  
     5.6      val lthy = Local_Theory.background_theory
     5.7 -      (Sign.add_consts_i ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) ::
     5.8 +      (Sign.add_consts ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) ::
     5.9          map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @
    5.10          map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs))
    5.11        lthy;
     6.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Mar 21 08:13:23 2014 +0100
     6.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Mar 21 10:45:03 2014 +0100
     6.3 @@ -761,7 +761,7 @@
     6.4            (Const (rep_name, T --> T') $ lhs, rhs));
     6.5          val def_name = (Long_Name.base_name cname) ^ "_def";
     6.6          val ([def_thm], thy') = thy |>
     6.7 -          Sign.add_consts_i [(cname', constrT, mx)] |>
     6.8 +          Sign.add_consts [(cname', constrT, mx)] |>
     6.9            (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)];
    6.10        in (thy', defs @ [def_thm], eqns @ [eqn]) end;
    6.11  
    6.12 @@ -1993,7 +1993,7 @@
    6.13  
    6.14      val (reccomb_defs, thy12) =
    6.15        thy11
    6.16 -      |> Sign.add_consts_i (map (fn ((name, T), T') =>
    6.17 +      |> Sign.add_consts (map (fn ((name, T), T') =>
    6.18            (Binding.name (Long_Name.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
    6.19            (reccomb_names ~~ recTs ~~ rec_result_Ts))
    6.20        |> (Global_Theory.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
     7.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Mar 21 08:13:23 2014 +0100
     7.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Mar 21 10:45:03 2014 +0100
     7.3 @@ -1001,7 +1001,7 @@
     7.4    in
     7.5      (c,
     7.6       ((Symtab.update (s, (c, ty)) tab, Name.declare s ctxt),
     7.7 -      Sign.add_consts_i [(b, T, NoSyn)] thy))
     7.8 +      Sign.add_consts [(b, T, NoSyn)] thy))
     7.9    end;
    7.10  
    7.11  fun add_def prfx types pfuns consts (id, (s, e)) (ids as (tab, ctxt), thy) =
     8.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Fri Mar 21 08:13:23 2014 +0100
     8.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Mar 21 10:45:03 2014 +0100
     8.3 @@ -237,7 +237,7 @@
     8.4            HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (Rep_name, T --> Univ_elT) $ lhs, rhs));
     8.5          val ([def_thm], thy') =
     8.6            thy
     8.7 -          |> Sign.add_consts_i [(cname', constrT, mx)]
     8.8 +          |> Sign.add_consts [(cname', constrT, mx)]
     8.9            |> (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)];
    8.10  
    8.11        in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
    8.12 @@ -262,7 +262,7 @@
    8.13      val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) =
    8.14        fold dt_constr_defs
    8.15          (hd descr ~~ new_type_names ~~ map #2 typedefs ~~ newTs ~~ constr_syntax)
    8.16 -        (thy3 |> Sign.add_consts_i iso_decls |> Sign.parent_path, [], [], [], []);
    8.17 +        (thy3 |> Sign.add_consts iso_decls |> Sign.parent_path, [], [], [], []);
    8.18  
    8.19  
    8.20      (*********** isomorphisms for new types (introduced by typedef) ***********)
     9.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Mar 21 08:13:23 2014 +0100
     9.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Mar 21 10:45:03 2014 +0100
     9.3 @@ -226,7 +226,7 @@
     9.4  
     9.5      val (reccomb_defs, thy2) =
     9.6        thy1
     9.7 -      |> Sign.add_consts_i (map (fn ((name, T), T') =>
     9.8 +      |> Sign.add_consts (map (fn ((name, T), T') =>
     9.9              (Binding.name (Long_Name.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn))
    9.10              (reccomb_names ~~ recTs ~~ rec_result_Ts))
    9.11        |> (Global_Theory.add_defs false o map Thm.no_attributes)
    10.1 --- a/src/HOL/Tools/Function/size.ML	Fri Mar 21 08:13:23 2014 +0100
    10.2 +++ b/src/HOL/Tools/Function/size.ML	Fri Mar 21 10:45:03 2014 +0100
    10.3 @@ -134,7 +134,7 @@
    10.4  
    10.5      val ((size_def_thms, size_def_thms'), thy') =
    10.6        thy
    10.7 -      |> Sign.add_consts_i (map (fn (s, T) =>
    10.8 +      |> Sign.add_consts (map (fn (s, T) =>
    10.9             (Binding.name (Long_Name.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
   10.10             (size_names ~~ recTs1))
   10.11        |> Global_Theory.add_defs false
    11.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Mar 21 08:13:23 2014 +0100
    11.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Mar 21 10:45:03 2014 +0100
    11.3 @@ -1212,7 +1212,7 @@
    11.4      val constname = "quickcheck"
    11.5      val full_constname = Sign.full_bname thy constname
    11.6      val constT = map snd vs' ---> @{typ bool}
    11.7 -    val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
    11.8 +    val thy1 = Sign.add_consts [(Binding.name constname, constT, NoSyn)] thy
    11.9      val const = Const (full_constname, constT)
   11.10      val t =
   11.11        Logic.list_implies
    12.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Mar 21 08:13:23 2014 +0100
    12.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Mar 21 10:45:03 2014 +0100
    12.3 @@ -1146,7 +1146,7 @@
    12.4          val lhs = Const (mode_cname, funT)
    12.5          val def = Logic.mk_equals (lhs, predterm)
    12.6          val ([definition], thy') = thy |>
    12.7 -          Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
    12.8 +          Sign.add_consts [(Binding.name mode_cbasename, funT, NoSyn)] |>
    12.9            Global_Theory.add_defs false [((Binding.name (Thm.def_name mode_cbasename), def), [])]
   12.10          val ctxt' = Proof_Context.init_global thy'
   12.11          val rules as ((intro, elim), _) =
   12.12 @@ -1171,7 +1171,7 @@
   12.13          val mode_cname = create_constname_of_mode options thy function_name_prefix name T mode
   12.14          val funT = Comp_Mod.funT_of comp_modifiers mode T
   12.15        in
   12.16 -        thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
   12.17 +        thy |> Sign.add_consts [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
   12.18          |> set_function_name (Comp_Mod.compilation comp_modifiers) name mode mode_cname
   12.19        end;
   12.20    in
    13.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Fri Mar 21 08:13:23 2014 +0100
    13.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Fri Mar 21 10:45:03 2014 +0100
    13.3 @@ -284,7 +284,7 @@
    13.4            end
    13.5        val intr_tss = map mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss))
    13.6        val (intrs, thy') = thy
    13.7 -        |> Sign.add_consts_i
    13.8 +        |> Sign.add_consts
    13.9            (map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn))
   13.10             dst_preds)
   13.11          |> fold_map Specification.axiom  (* FIXME !?!?!?! *)
    14.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Mar 21 08:13:23 2014 +0100
    14.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Mar 21 10:45:03 2014 +0100
    14.3 @@ -87,7 +87,7 @@
    14.4        val lhs = list_comb (Const (full_constname, constT), params @ args)
    14.5        val def = Logic.mk_equals (lhs, atom)
    14.6        val ([definition], thy') = thy
    14.7 -        |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
    14.8 +        |> Sign.add_consts [(Binding.name constname, constT, NoSyn)]
    14.9          |> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])]
   14.10      in
   14.11        (lhs, ((full_constname, [definition]) :: defs, thy'))
   14.12 @@ -119,7 +119,7 @@
   14.13                  Logic.mk_equals (fold Envir.expand_term_frees (map single subst) lhs, rhs)
   14.14                val new_defs = map mk_def srs
   14.15                val (definition, thy') = thy
   14.16 -              |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
   14.17 +              |> Sign.add_consts [(Binding.name constname, constT, NoSyn)]
   14.18                |> fold_map Specification.axiom  (* FIXME !?!?!?! *)
   14.19                  (map_index (fn (i, t) =>
   14.20                    ((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs)
   14.21 @@ -245,7 +245,7 @@
   14.22              val lhs = list_comb (const, frees)
   14.23              val def = Logic.mk_equals (lhs, abs_arg')
   14.24              val ([definition], thy') = thy
   14.25 -              |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
   14.26 +              |> Sign.add_consts [(Binding.name constname, constT, NoSyn)]
   14.27                |> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])]
   14.28            in
   14.29              (list_comb (Logic.varify_global const, vars),
    15.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Fri Mar 21 08:13:23 2014 +0100
    15.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Fri Mar 21 10:45:03 2014 +0100
    15.3 @@ -94,7 +94,7 @@
    15.4        end handle Pattern.Unif => NONE)
    15.5      val specialised_intros_t = map_filter I (map specialise_intro intros)
    15.6      val thy' =
    15.7 -      Sign.add_consts_i [(Binding.name (Long_Name.base_name constname), constT, NoSyn)] thy
    15.8 +      Sign.add_consts [(Binding.name (Long_Name.base_name constname), constT, NoSyn)] thy
    15.9      val specialised_intros = map (Skip_Proof.make_thm thy') specialised_intros_t
   15.10      val exported_intros = Variable.exportT ctxt' ctxt specialised_intros
   15.11      val [t, specialised_t] = Variable.exportT_terms ctxt' ctxt
    16.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Mar 21 08:13:23 2014 +0100
    16.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Mar 21 10:45:03 2014 +0100
    16.3 @@ -108,7 +108,7 @@
    16.4  
    16.5  val _ =
    16.6    Outer_Syntax.command @{command_spec "consts"} "declare constants"
    16.7 -    (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts));
    16.8 +    (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd));
    16.9  
   16.10  val mode_spec =
   16.11    (@{keyword "output"} >> K ("", false)) ||
   16.12 @@ -119,11 +119,13 @@
   16.13  
   16.14  val _ =
   16.15    Outer_Syntax.command @{command_spec "syntax"} "add raw syntax clauses"
   16.16 -    (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_modesyntax));
   16.17 +    (opt_mode -- Scan.repeat1 Parse.const_decl
   16.18 +      >> (Toplevel.theory o uncurry Sign.add_modesyntax_cmd));
   16.19  
   16.20  val _ =
   16.21    Outer_Syntax.command @{command_spec "no_syntax"} "delete raw syntax clauses"
   16.22 -    (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_modesyntax));
   16.23 +    (opt_mode -- Scan.repeat1 Parse.const_decl
   16.24 +      >> (Toplevel.theory o uncurry Sign.del_modesyntax_cmd));
   16.25  
   16.26  
   16.27  (* translations *)
    17.1 --- a/src/Pure/Isar/object_logic.ML	Fri Mar 21 08:13:23 2014 +0100
    17.2 +++ b/src/Pure/Isar/object_logic.ML	Fri Mar 21 10:45:03 2014 +0100
    17.3 @@ -97,8 +97,8 @@
    17.4  
    17.5  in
    17.6  
    17.7 -val add_judgment = gen_add_judgment Sign.add_consts_i;
    17.8 -val add_judgment_cmd = gen_add_judgment Sign.add_consts;
    17.9 +val add_judgment = gen_add_judgment Sign.add_consts;
   17.10 +val add_judgment_cmd = gen_add_judgment Sign.add_consts_cmd;
   17.11  
   17.12  end;
   17.13  
    18.1 --- a/src/Pure/Proof/extraction.ML	Fri Mar 21 08:13:23 2014 +0100
    18.2 +++ b/src/Pure/Proof/extraction.ML	Fri Mar 21 10:45:03 2014 +0100
    18.3 @@ -37,7 +37,7 @@
    18.4  val add_syntax =
    18.5    Sign.root_path
    18.6    #> Sign.add_types_global [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)]
    18.7 -  #> Sign.add_consts_i
    18.8 +  #> Sign.add_consts
    18.9        [(Binding.name "typeof", typ "'b => Type", NoSyn),
   18.10         (Binding.name "Type", typ "'a itself => Type", NoSyn),
   18.11         (Binding.name "Null", typ "Null", NoSyn),
   18.12 @@ -791,7 +791,7 @@
   18.13               val fu = Type.legacy_freeze u;
   18.14               val (def_thms, thy') = if t = nullt then ([], thy) else
   18.15                 thy
   18.16 -               |> Sign.add_consts_i [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
   18.17 +               |> Sign.add_consts [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
   18.18                 |> Global_Theory.add_defs false
   18.19                    [((Binding.qualified_name (Thm.def_name (extr_name s vs)),
   18.20                      Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
    19.1 --- a/src/Pure/Proof/proof_syntax.ML	Fri Mar 21 08:13:23 2014 +0100
    19.2 +++ b/src/Pure/Proof/proof_syntax.ML	Fri Mar 21 10:45:03 2014 +0100
    19.3 @@ -35,7 +35,7 @@
    19.4  fun add_proof_atom_consts names thy =
    19.5    thy
    19.6    |> Sign.root_path
    19.7 -  |> Sign.add_consts_i (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names);
    19.8 +  |> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names);
    19.9  
   19.10  (** constants for application and abstraction **)
   19.11  
   19.12 @@ -54,7 +54,7 @@
   19.13         ((Binding.name "OfClass", (Term.a_itselfT --> propT) --> proofT), NoSyn),
   19.14         ((Binding.name "MinProof", proofT), Delimfix "?")]
   19.15    |> Sign.add_nonterminals_global [Binding.name "param", Binding.name "params"]
   19.16 -  |> Sign.add_syntax_i
   19.17 +  |> Sign.add_syntax
   19.18        [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
   19.19         ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
   19.20         ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
   19.21 @@ -62,7 +62,7 @@
   19.22         ("", paramT --> paramT, Delimfix "'(_')"),
   19.23         ("", idtT --> paramsT, Delimfix "_"),
   19.24         ("", paramT --> paramsT, Delimfix "_")]
   19.25 -  |> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
   19.26 +  |> Sign.add_modesyntax (Symbol.xsymbolsN, true)
   19.27        [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
   19.28         (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
   19.29         (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \<bullet>/ _)", [4, 5], 4))]
    20.1 --- a/src/Pure/pure_thy.ML	Fri Mar 21 08:13:23 2014 +0100
    20.2 +++ b/src/Pure/pure_thy.ML	Fri Mar 21 10:45:03 2014 +0100
    20.3 @@ -49,8 +49,8 @@
    20.4  
    20.5  val old_appl_syntax_setup =
    20.6    Old_Appl_Syntax.put true #>
    20.7 -  Sign.del_modesyntax_i Syntax.mode_default applC_syntax #>
    20.8 -  Sign.add_syntax_i appl_syntax;
    20.9 +  Sign.del_modesyntax Syntax.mode_default applC_syntax #>
   20.10 +  Sign.add_syntax appl_syntax;
   20.11  
   20.12  
   20.13  (* main content *)
   20.14 @@ -75,8 +75,8 @@
   20.15          "tvar_position", "id_position", "longid_position", "var_position",
   20.16          "str_position", "string_position", "cartouche_position", "type_name",
   20.17          "class_name"]))
   20.18 -  #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) token_markers)
   20.19 -  #> Sign.add_syntax_i
   20.20 +  #> Sign.add_syntax (map (fn x => (x, typ "'a", NoSyn)) token_markers)
   20.21 +  #> Sign.add_syntax
   20.22     [("",            typ "prop' => prop",               Delimfix "_"),
   20.23      ("",            typ "logic => any",                Delimfix "_"),
   20.24      ("",            typ "prop' => any",                Delimfix "_"),
   20.25 @@ -174,8 +174,8 @@
   20.26      ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
   20.27      (const "Pure.term", typ "logic => prop",           Delimfix "TERM _"),
   20.28      (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
   20.29 -  #> Sign.add_syntax_i applC_syntax
   20.30 -  #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
   20.31 +  #> Sign.add_syntax applC_syntax
   20.32 +  #> Sign.add_modesyntax (Symbol.xsymbolsN, true)
   20.33     [(tycon "fun",         typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
   20.34      ("_bracket",          typ "types => type => type",  Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
   20.35      ("_ofsort",           typ "tid_position => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
   20.36 @@ -190,11 +190,11 @@
   20.37      ("_DDDOT",            typ "aprop",                  Delimfix "\\<dots>"),
   20.38      ("_bigimpl",          typ "asms => prop => prop",   Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
   20.39      ("_DDDOT",            typ "logic",                  Delimfix "\\<dots>")]
   20.40 -  #> Sign.add_modesyntax_i ("", false)
   20.41 +  #> Sign.add_modesyntax ("", false)
   20.42     [(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))]
   20.43 -  #> Sign.add_modesyntax_i ("HTML", false)
   20.44 +  #> Sign.add_modesyntax ("HTML", false)
   20.45     [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
   20.46 -  #> Sign.add_consts_i
   20.47 +  #> Sign.add_consts
   20.48     [(Binding.name "==", typ "'a => 'a => prop", Infix ("==", 2)),
   20.49      (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
   20.50      (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
   20.51 @@ -209,7 +209,7 @@
   20.52    #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
   20.53    #> Sign.parse_translation Syntax_Trans.pure_parse_translation
   20.54    #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
   20.55 -  #> Sign.add_consts_i
   20.56 +  #> Sign.add_consts
   20.57     [(qualify (Binding.name "term"), typ "'a => prop", NoSyn),
   20.58      (qualify (Binding.name "sort_constraint"), typ "'a itself => prop", NoSyn),
   20.59      (qualify (Binding.name "conjunction"), typ "prop => prop => prop", NoSyn)]
    21.1 --- a/src/Pure/sign.ML	Fri Mar 21 08:13:23 2014 +0100
    21.2 +++ b/src/Pure/sign.ML	Fri Mar 21 10:45:03 2014 +0100
    21.3 @@ -73,18 +73,18 @@
    21.4    val add_nonterminals: Proof.context -> binding list -> theory -> theory
    21.5    val add_nonterminals_global: binding list -> theory -> theory
    21.6    val add_type_abbrev: Proof.context -> binding * string list * typ -> theory -> theory
    21.7 -  val add_syntax: (string * string * mixfix) list -> theory -> theory
    21.8 -  val add_syntax_i: (string * typ * mixfix) list -> theory -> theory
    21.9 -  val add_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
   21.10 -  val add_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
   21.11 -  val del_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
   21.12 -  val del_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
   21.13 +  val add_syntax: (string * typ * mixfix) list -> theory -> theory
   21.14 +  val add_syntax_cmd: (string * string * mixfix) list -> theory -> theory
   21.15 +  val add_modesyntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
   21.16 +  val add_modesyntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
   21.17 +  val del_modesyntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
   21.18 +  val del_modesyntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
   21.19    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory
   21.20    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
   21.21    val declare_const: Proof.context -> (binding * typ) * mixfix -> theory -> term * theory
   21.22    val declare_const_global: (binding * typ) * mixfix -> theory -> term * theory
   21.23 -  val add_consts: (binding * string * mixfix) list -> theory -> theory
   21.24 -  val add_consts_i: (binding * typ * mixfix) list -> theory -> theory
   21.25 +  val add_consts: (binding * typ * mixfix) list -> theory -> theory
   21.26 +  val add_consts_cmd: (binding * string * mixfix) list -> theory -> theory
   21.27    val add_abbrev: string -> binding * term -> theory -> (term * term) * theory
   21.28    val revert_abbrev: string -> string -> theory -> theory
   21.29    val add_const_constraint: string * typ option -> theory -> theory
   21.30 @@ -375,12 +375,12 @@
   21.31  
   21.32  fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x;
   21.33  
   21.34 -val add_modesyntax = gen_add_syntax Syntax.read_typ;
   21.35 -val add_modesyntax_i = gen_add_syntax (K I);
   21.36 +val add_modesyntax = gen_add_syntax (K I);
   21.37 +val add_modesyntax_cmd = gen_add_syntax Syntax.read_typ;
   21.38  val add_syntax = add_modesyntax Syntax.mode_default;
   21.39 -val add_syntax_i = add_modesyntax_i Syntax.mode_default;
   21.40 -val del_modesyntax = gen_syntax (Syntax.update_const_gram false) Syntax.read_typ;
   21.41 -val del_modesyntax_i = gen_syntax (Syntax.update_const_gram false) (K I);
   21.42 +val add_syntax_cmd = add_modesyntax_cmd Syntax.mode_default;
   21.43 +val del_modesyntax = gen_syntax (Syntax.update_const_gram false) (K I);
   21.44 +val del_modesyntax_cmd = gen_syntax (Syntax.update_const_gram false) Syntax.read_typ;
   21.45  
   21.46  fun type_notation add mode args =
   21.47    let
   21.48 @@ -417,17 +417,17 @@
   21.49    in
   21.50      thy
   21.51      |> map_consts (fold (Consts.declare (inherit_naming thy ctxt) o #1) args)
   21.52 -    |> add_syntax_i (map #2 args)
   21.53 +    |> add_syntax (map #2 args)
   21.54      |> pair (map #3 args)
   21.55    end;
   21.56  
   21.57  in
   21.58  
   21.59  fun add_consts args thy =
   21.60 -  #2 (gen_add_consts Syntax.read_typ (Proof_Context.init_global thy) args thy);
   21.61 +  #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy);
   21.62  
   21.63 -fun add_consts_i args thy =
   21.64 -  #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy);
   21.65 +fun add_consts_cmd args thy =
   21.66 +  #2 (gen_add_consts Syntax.read_typ (Proof_Context.init_global thy) args thy);
   21.67  
   21.68  fun declare_const ctxt ((b, T), mx) = yield_singleton (gen_add_consts (K I) ctxt) (b, T, mx);
   21.69  fun declare_const_global arg thy = declare_const (Proof_Context.init_global thy) arg thy;
   21.70 @@ -468,7 +468,7 @@
   21.71    |> map_sign (fn (syn, tsig, consts) =>
   21.72        let val tsig' = Type.add_class (Context.Theory thy) (bclass, classes) tsig;
   21.73        in (syn, tsig', consts) end)
   21.74 -  |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
   21.75 +  |> add_consts [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
   21.76  
   21.77  fun primitive_classrel arg thy =
   21.78    thy |> map_tsig (Type.add_classrel (Context.pretty_global thy) arg);
    22.1 --- a/src/ZF/Tools/datatype_package.ML	Fri Mar 21 08:13:23 2014 +0100
    22.2 +++ b/src/ZF/Tools/datatype_package.ML	Fri Mar 21 10:45:03 2014 +0100
    22.3 @@ -244,21 +244,20 @@
    22.4    fun add_recursor thy =
    22.5      if need_recursor then
    22.6        thy
    22.7 -      |> Sign.add_consts_i
    22.8 -        [(Binding.name recursor_base_name, recursor_typ, NoSyn)]
    22.9 +      |> Sign.add_consts [(Binding.name recursor_base_name, recursor_typ, NoSyn)]
   22.10        |> (snd o Global_Theory.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
   22.11      else thy;
   22.12  
   22.13    val (con_defs, thy0) = thy_path
   22.14 -             |> Sign.add_consts_i
   22.15 -                 (map (fn (c, T, mx) => (Binding.name c, T, mx))
   22.16 -                  ((case_base_name, case_typ, NoSyn) :: map #1 (flat con_ty_lists)))
   22.17 -             |> Global_Theory.add_defs false
   22.18 -                 (map (Thm.no_attributes o apfst Binding.name)
   22.19 -                  (case_def ::
   22.20 -                   flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists))))
   22.21 -             ||> add_recursor
   22.22 -             ||> Sign.parent_path
   22.23 +    |> Sign.add_consts
   22.24 +        (map (fn (c, T, mx) => (Binding.name c, T, mx))
   22.25 +         ((case_base_name, case_typ, NoSyn) :: map #1 (flat con_ty_lists)))
   22.26 +    |> Global_Theory.add_defs false
   22.27 +        (map (Thm.no_attributes o apfst Binding.name)
   22.28 +         (case_def ::
   22.29 +          flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists))))
   22.30 +    ||> add_recursor
   22.31 +    ||> Sign.parent_path;
   22.32  
   22.33    val intr_names = map (Binding.name o #2) (flat con_ty_lists);
   22.34    val (thy1, ind_result) =