--- 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
--- 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