# HG changeset patch
# User wenzelm
# Date 1165510719 -3600
# Node ID 826ab43d43f5a6cb9c69a6747f705bb5982f6f88
# Parent  552d20ff9a9508a6e51dccea581c00c2525cb9d3
TermSyntax.notation/abbrevs;

diff -r 552d20ff9a95 -r 826ab43d43f5 src/HOL/Tools/function_package/fundef_prep.ML
--- 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
diff -r 552d20ff9a95 -r 826ab43d43f5 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Dec 07 16:47:36 2006 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Dec 07 17:58:39 2006 +0100
@@ -157,7 +157,7 @@
         val mx = (case vars of [] => NoSyn | [((y, _), mx)] =>
           if x = y then mx
           else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y));
-        val lthy2 = lthy1 |> LocalTheory.abbrevs mode [((x, mx), rhs)];
+        val lthy2 = lthy1 |> TermSyntax.abbrevs mode [((x, mx), rhs)];
       in ((x, T), LocalTheory.restore lthy2) end;
 
     val (cs, lthy') = lthy
@@ -174,7 +174,7 @@
 (* notation *)
 
 fun gen_notation prep_const mode args lthy =
-  lthy |> LocalTheory.notation mode (map (apfst (prep_const lthy)) args);
+  lthy |> TermSyntax.notation mode (map (apfst (prep_const lthy)) args);
 
 val notation = gen_notation ProofContext.read_const;
 val notation_i = gen_notation (K I);
diff -r 552d20ff9a95 -r 826ab43d43f5 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Thu Dec 07 16:47:36 2006 +0100
+++ b/src/Pure/Isar/theory_target.ML	Thu Dec 07 17:58:39 2006 +0100
@@ -72,7 +72,7 @@
     val defs = abbrs |> map (fn (x, t) => (x, (("", []), t)));
   in
     lthy'
-    |> is_loc ? LocalTheory.abbrevs Syntax.default_mode abbrs
+    |> is_loc ? TermSyntax.abbrevs Syntax.default_mode abbrs
     |> LocalDefs.add_defs defs |>> map (apsnd snd)
   end;