# HG changeset patch
# User wenzelm
# Date 1192111526 -7200
# Node ID 39d1dd215d7326d4f951b2e2910770e55d121084
# Parent  119793c846479e3fa9065076f0bc91e3249e84c0
renamed Syntax.XXX_mode to Syntax.mode_XXX;

diff -r 119793c84647 -r 39d1dd215d73 src/HOL/Tools/function_package/fundef_core.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
diff -r 119793c84647 -r 39d1dd215d73 src/HOL/Tools/inductive_package.ML
--- 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 =
diff -r 119793c84647 -r 39d1dd215d73 src/Pure/Isar/isar_syn.ML
--- 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
diff -r 119793c84647 -r 39d1dd215d73 src/Pure/Isar/local_syntax.ML
--- 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
diff -r 119793c84647 -r 39d1dd215d73 src/Pure/pure_setup.ML
--- 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;