renamed Syntax.XXX_mode to Syntax.mode_XXX;
authorwenzelm
Thu Oct 11 16:05:26 2007 +0200 (2007-10-11)
changeset 2496039d1dd215d73
parent 24959 119793c84647
child 24961 5298ee9c3fe5
renamed Syntax.XXX_mode to Syntax.mode_XXX;
src/HOL/Tools/function_package/fundef_core.ML
src/HOL/Tools/inductive_package.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/local_syntax.ML
src/Pure/pure_setup.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_core.ML	Thu Oct 11 16:05:23 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_core.ML	Thu Oct 11 16:05:26 2007 +0200
     1.3 @@ -896,7 +896,7 @@
     1.4            PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
     1.5  
     1.6        val (_, lthy) = 
     1.7 -          LocalTheory.abbrev Syntax.default_mode ((dom_name defname, NoSyn), mk_acc domT R) lthy
     1.8 +          LocalTheory.abbrev Syntax.mode_default ((dom_name defname, NoSyn), mk_acc domT R) lthy
     1.9  
    1.10        val newthy = ProofContext.theory_of lthy
    1.11        val clauses = map (transfer_clause_ctx newthy) clauses
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Oct 11 16:05:23 2007 +0200
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Oct 11 16:05:26 2007 +0200
     2.3 @@ -829,7 +829,7 @@
     2.4    in
     2.5      ctxt
     2.6      |> mk_def flags cs intros monos params cnames_syn''
     2.7 -    ||> fold (snd oo LocalTheory.abbrev Syntax.default_mode) abbrevs''
     2.8 +    ||> fold (snd oo LocalTheory.abbrev Syntax.mode_default) abbrevs''
     2.9    end;
    2.10  
    2.11  fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos lthy =
     3.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Oct 11 16:05:23 2007 +0200
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Oct 11 16:05:26 2007 +0200
     3.3 @@ -151,7 +151,7 @@
     3.4    (P.$$$ "output" >> K ("", false)) || P.name -- Scan.optional (P.$$$ "output" >> K false) true;
     3.5  
     3.6  val opt_mode =
     3.7 -  Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) Syntax.default_mode;
     3.8 +  Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) Syntax.mode_default;
     3.9  
    3.10  val _ =
    3.11    OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
     4.1 --- a/src/Pure/Isar/local_syntax.ML	Thu Oct 11 16:05:23 2007 +0200
     4.2 +++ b/src/Pure/Isar/local_syntax.ML	Thu Oct 11 16:05:26 2007 +0200
     4.3 @@ -69,7 +69,7 @@
     4.4        |> fold const_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
     4.5    in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
     4.6  
     4.7 -fun init thy = build_syntax thy Syntax.default_mode [] ([], []);
     4.8 +fun init thy = build_syntax thy Syntax.mode_default [] ([], []);
     4.9  
    4.10  fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) =
    4.11    if is_consistent thy syntax then syntax
     5.1 --- a/src/Pure/pure_setup.ML	Thu Oct 11 16:05:23 2007 +0200
     5.2 +++ b/src/Pure/pure_setup.ML	Thu Oct 11 16:05:26 2007 +0200
     5.3 @@ -20,7 +20,7 @@
     5.4  structure Pure = struct val thy = theory "Pure" end;
     5.5  
     5.6  Context.add_setup
     5.7 - (Sign.del_modesyntax_i Syntax.default_mode PureThy.appl_syntax #>
     5.8 + (Sign.del_modesyntax_i Syntax.mode_default PureThy.appl_syntax #>
     5.9    Sign.add_syntax_i PureThy.applC_syntax);
    5.10  use_thy "CPure";
    5.11  structure CPure = struct val thy = theory "CPure" end;