--- a/src/HOL/Tools/function_package/fundef_prep.ML Sat Dec 09 18:05:36 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_prep.ML Sat Dec 09 18:05:37 2006 +0100
@@ -508,7 +508,7 @@
PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
val lthy = PROFILE "abbrev"
- (TermSyntax.abbrevs Syntax.default_mode [((defname ^ "_dom", NoSyn), mk_acc domT R)]) lthy
+ (TermSyntax.abbrev 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
--- a/src/Pure/Isar/theory_target.ML Sat Dec 09 18:05:36 2006 +0100
+++ b/src/Pure/Isar/theory_target.ML Sat Dec 09 18:05:37 2006 +0100
@@ -72,7 +72,7 @@
val defs = abbrs |> map (fn (x, t) => (x, (("", []), t)));
in
lthy'
- |> is_loc ? TermSyntax.abbrevs Syntax.default_mode abbrs
+ |> is_loc ? fold (TermSyntax.abbrev Syntax.internal_mode) abbrs
|> LocalDefs.add_defs defs |>> map (apsnd snd)
end;