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