--- 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;