# HG changeset patch
# User wenzelm
# Date 1164560841 -3600
# Node ID 7140f8aba3801c1414c219be77335131773b63cf
# Parent  1e6bd5ed7abc74b85d556547d6c0257756199366
abbrevs: no result;

diff -r 1e6bd5ed7abc -r 7140f8aba380 src/HOL/Tools/function_package/fundef_prep.ML
--- a/src/HOL/Tools/function_package/fundef_prep.ML	Sun Nov 26 18:07:20 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_prep.ML	Sun Nov 26 18:07:21 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"
-        (snd o LocalTheory.abbrevs ("", false) (* FIXME really this mode? cf. Syntax.default_mode *)
+        (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
diff -r 1e6bd5ed7abc -r 7140f8aba380 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Nov 26 18:07:20 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Nov 26 18:07:21 2006 +0100
@@ -215,7 +215,7 @@
     (P.opt_locale_target -- opt_mode --
       Scan.repeat1 (Scan.option constdecl -- P.prop)
     >> (fn ((loc, mode), args) =>
-        Toplevel.local_theory loc (snd o Specification.abbreviation mode args)));
+        Toplevel.local_theory loc (Specification.abbreviation mode args)));
 
 val notationP =
   OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl