# HG changeset patch
# User wenzelm
# Date 1165683937 -3600
# Node ID 43b935d6fb5a726c3915418b3372be8e7c769cec
# Parent  410ca6910f6ff9b0b95237e5aa047fbf72b47df5
TermSyntax.abbrev;

diff -r 410ca6910f6f -r 43b935d6fb5a src/HOL/Tools/function_package/fundef_prep.ML
--- 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
diff -r 410ca6910f6f -r 43b935d6fb5a src/Pure/Isar/theory_target.ML
--- 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;