# HG changeset patch
# User wenzelm
# Date 1165761045 -3600
# Node ID 9d0652354513b4c79341a930b06897e68a5065bb
# Parent  a1d8806b5267938877ad903d4a45994c86c3c283
LocalTheory.notation/abbrev;

diff -r a1d8806b5267 -r 9d0652354513 src/HOL/Tools/function_package/fundef_prep.ML
--- a/src/HOL/Tools/function_package/fundef_prep.ML	Sun Dec 10 15:30:44 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_prep.ML	Sun Dec 10 15:30:45 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.abbrev Syntax.default_mode ((defname ^ "_dom", NoSyn), mk_acc domT R)) lthy
+        (LocalTheory.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 a1d8806b5267 -r 9d0652354513 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun Dec 10 15:30:44 2006 +0100
+++ b/src/Pure/Isar/specification.ML	Sun Dec 10 15:30:45 2006 +0100
@@ -153,7 +153,7 @@
       else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y));
     val lthy' = lthy
       |> ProofContext.set_syntax_mode mode    (* FIXME !? *)
-      |> TermSyntax.abbrev mode ((x, mx), rhs)
+      |> LocalTheory.abbrev mode ((x, mx), rhs)
       |> ProofContext.restore_syntax_mode lthy;
     val _ = print_consts lthy' (K false) [(x, T)]
   in lthy' end;
@@ -165,7 +165,7 @@
 (* notation *)
 
 fun gen_notation prep_const mode args lthy =
-  lthy |> TermSyntax.notation mode (map (apfst (prep_const lthy)) args);
+  lthy |> LocalTheory.notation mode (map (apfst (prep_const lthy)) args);
 
 val notation = gen_notation ProofContext.read_const;
 val notation_i = gen_notation (K I);