# HG changeset patch
# User wenzelm
# Date 1163105069 -3600
# Node ID 4f791faf33f41391e8dcf768f5126bbab809bcdb
# Parent  b82f4c16355e85f08d682add2c93ae8280f10ff0
abbrevs: return result (use LocalTheory.abbrevs directly);

diff -r b82f4c16355e -r 4f791faf33f4 src/HOL/Tools/function_package/fundef_prep.ML
--- a/src/HOL/Tools/function_package/fundef_prep.ML	Thu Nov 09 21:44:28 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_prep.ML	Thu Nov 09 21:44:29 2006 +0100
@@ -508,8 +508,9 @@
       val ((R, RIntro_thmss, R_elim), lthy) = 
           PROFILE "def_rel" (define_recursion_relation (defname ^ "_rel") domT ranT fvar f abstract_qglrs clauses RCss) lthy
 
-      val dom_abbrev = Logic.mk_equals (Free (defname ^ "_dom", domT --> boolT), mk_acc domT R)
-      val lthy = PROFILE "abbrev" (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) lthy
+      val lthy = PROFILE "abbrev"
+        (snd o LocalTheory.abbrevs ("", false) (* FIXME really this mode? cf. 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