# HG changeset patch
# User wenzelm
# Date 1192899268 -7200
# Node ID 7aa178165ee4aeb595e7de5b644df276720736f2
# Parent  008c964dd47f5cfd07d2e757ef978be465b915eb
add_inductive: more careful handling of abbrevs -- do not expand prematurely;

diff -r 008c964dd47f -r 7aa178165ee4 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Sat Oct 20 15:46:04 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Sat Oct 20 18:54:28 2007 +0200
@@ -815,8 +815,8 @@
 
     val ctxt2 = lthy
       |> Variable.add_fixes (map (fst o fst) cnames_syn') |> snd
-      |> fold (snd oo LocalDefs.add_def) abbrevs;
-    val expand = Assumption.export_term ctxt2 lthy;
+      |> fold (snd oo LocalDefs.fixed_abbrev) abbrevs;
+    val expand = Assumption.export_term ctxt2 lthy #> ProofContext.cert_term lthy;
 
     fun close_rule r = list_all_free (rev (fold_aterms
       (fn t as Free (v as (s, _)) =>
@@ -834,8 +834,9 @@
 
 fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos lthy =
   let
-    val ((vars, specs), _) = lthy |> Specification.read_specification
-      (cnames_syn @ pnames_syn) (map (fn (a, s) => [(a, [s])]) intro_srcs);
+    val ((vars, specs), _) = lthy |> ProofContext.set_mode ProofContext.mode_abbrev
+      |> Specification.read_specification
+          (cnames_syn @ pnames_syn) (map (fn (a, s) => [(a, [s])]) intro_srcs);
     val (cs, ps) = chop (length cnames_syn) vars;
     val intrs = map (apsnd the_single) specs;
     val monos = Attrib.eval_thms lthy raw_monos;