# HG changeset patch
# User wenzelm
# Date 1165952959 -3600
# Node ID 74409847e349b065ab07a83e67e41afeeb4cf1fb
# Parent  266a1056a2a312cdab094a29ddea69edaf185d23
LocalTheory.abbrev;

diff -r 266a1056a2a3 -r 74409847e349 src/HOL/Tools/function_package/fundef_prep.ML
--- a/src/HOL/Tools/function_package/fundef_prep.ML	Tue Dec 12 17:29:26 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_prep.ML	Tue Dec 12 20:49:19 2006 +0100
@@ -507,7 +507,7 @@
       val ((R, RIntro_thmss, R_elim), lthy) = 
           PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
 
-      val lthy = PROFILE "abbrev"
+      val (_, lthy) = PROFILE "abbrev"
         (LocalTheory.abbrev Syntax.default_mode ((defname ^ "_dom", NoSyn), mk_acc domT R)) lthy
 
       val newthy = ProofContext.theory_of lthy
diff -r 266a1056a2a3 -r 74409847e349 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Tue Dec 12 17:29:26 2006 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Tue Dec 12 20:49:19 2006 +0100
@@ -789,7 +789,7 @@
     ctxt |>
     add_ind_def verbose alt_name coind no_elim no_ind cs intros monos
       params cnames_syn'' ||>
-    fold (LocalTheory.abbrev Syntax.default_mode) abbrevs''
+    fold (snd oo LocalTheory.abbrev Syntax.default_mode) abbrevs''
   end;
 
 fun add_inductive verbose coind cnames_syn pnames_syn intro_srcs raw_monos ctxt =
diff -r 266a1056a2a3 -r 74409847e349 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue Dec 12 17:29:26 2006 +0100
+++ b/src/Pure/Isar/specification.ML	Tue Dec 12 20:49:19 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 !? *)
-      |> LocalTheory.abbrev mode ((x, mx), rhs)
+      |> LocalTheory.abbrev mode ((x, mx), rhs) |> snd
       |> ProofContext.restore_syntax_mode lthy;
     val _ = print_consts lthy' (K false) [(x, T)]
   in lthy' end;