renamed Syntax.XXX_mode to Syntax.mode_XXX;
authorwenzelm
Thu, 11 Oct 2007 16:05:26 +0200
changeset 24960 39d1dd215d73
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
--- a/src/HOL/Tools/function_package/fundef_core.ML	Thu Oct 11 16:05:23 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_core.ML	Thu Oct 11 16:05:26 2007 +0200
@@ -896,7 +896,7 @@
           PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
 
       val (_, lthy) = 
-          LocalTheory.abbrev Syntax.default_mode ((dom_name defname, NoSyn), mk_acc domT R) lthy
+          LocalTheory.abbrev Syntax.mode_default ((dom_name defname, NoSyn), mk_acc domT R) lthy
 
       val newthy = ProofContext.theory_of lthy
       val clauses = map (transfer_clause_ctx newthy) clauses
--- a/src/HOL/Tools/inductive_package.ML	Thu Oct 11 16:05:23 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Thu Oct 11 16:05:26 2007 +0200
@@ -829,7 +829,7 @@
   in
     ctxt
     |> mk_def flags cs intros monos params cnames_syn''
-    ||> fold (snd oo LocalTheory.abbrev Syntax.default_mode) abbrevs''
+    ||> fold (snd oo LocalTheory.abbrev Syntax.mode_default) abbrevs''
   end;
 
 fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos lthy =
--- a/src/Pure/Isar/isar_syn.ML	Thu Oct 11 16:05:23 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Oct 11 16:05:26 2007 +0200
@@ -151,7 +151,7 @@
   (P.$$$ "output" >> K ("", false)) || P.name -- Scan.optional (P.$$$ "output" >> K false) true;
 
 val opt_mode =
-  Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) Syntax.default_mode;
+  Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) Syntax.mode_default;
 
 val _ =
   OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
--- a/src/Pure/Isar/local_syntax.ML	Thu Oct 11 16:05:23 2007 +0200
+++ b/src/Pure/Isar/local_syntax.ML	Thu Oct 11 16:05:26 2007 +0200
@@ -69,7 +69,7 @@
       |> fold const_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
   in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
 
-fun init thy = build_syntax thy Syntax.default_mode [] ([], []);
+fun init thy = build_syntax thy Syntax.mode_default [] ([], []);
 
 fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) =
   if is_consistent thy syntax then syntax
--- a/src/Pure/pure_setup.ML	Thu Oct 11 16:05:23 2007 +0200
+++ b/src/Pure/pure_setup.ML	Thu Oct 11 16:05:26 2007 +0200
@@ -20,7 +20,7 @@
 structure Pure = struct val thy = theory "Pure" end;
 
 Context.add_setup
- (Sign.del_modesyntax_i Syntax.default_mode PureThy.appl_syntax #>
+ (Sign.del_modesyntax_i Syntax.mode_default PureThy.appl_syntax #>
   Sign.add_syntax_i PureThy.applC_syntax);
 use_thy "CPure";
 structure CPure = struct val thy = theory "CPure" end;