--- a/src/HOL/Tools/inductive.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/HOL/Tools/inductive.ML Sun Mar 07 11:57:16 2010 +0100
@@ -832,7 +832,7 @@
let
val _ = Binding.is_empty name andalso null atts orelse
error "Abbreviations may not have names or attributes";
- val ((x, T), rhs) = LocalDefs.abs_def (snd (LocalDefs.cert_def ctxt1 t));
+ val ((x, T), rhs) = Local_Defs.abs_def (snd (Local_Defs.cert_def ctxt1 t));
val var =
(case find_first (fn ((c, _), _) => Binding.name_of c = x) cnames_syn of
NONE => error ("Undeclared head of abbreviation " ^ quote x)
@@ -854,8 +854,8 @@
val ps = map Free pnames;
val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn');
- val _ = map (fn abbr => LocalDefs.fixed_abbrev abbr ctxt2) abbrevs;
- val ctxt3 = ctxt2 |> fold (snd oo LocalDefs.fixed_abbrev) abbrevs;
+ val _ = map (fn abbr => Local_Defs.fixed_abbrev abbr ctxt2) abbrevs;
+ val ctxt3 = ctxt2 |> fold (snd oo Local_Defs.fixed_abbrev) abbrevs;
val expand = Assumption.export_term ctxt3 lthy #> ProofContext.cert_term lthy;
fun close_rule r = list_all_free (rev (fold_aterms