--- a/src/HOL/Tools/function_package/fundef_prep.ML Thu Dec 07 16:47:36 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_prep.ML Thu Dec 07 17:58:39 2006 +0100
@@ -508,8 +508,7 @@
PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
val lthy = PROFILE "abbrev"
- (LocalTheory.abbrevs ("", false) (* FIXME really this mode? cf. Syntax.default_mode *)
- [((defname ^ "_dom", NoSyn), mk_acc domT R)]) lthy
+ (TermSyntax.abbrevs Syntax.default_mode [((defname ^ "_dom", NoSyn), mk_acc domT R)]) lthy
val newthy = ProofContext.theory_of lthy
val clauses = map (transfer_clause_ctx newthy) clauses