--- a/src/Pure/Isar/local_defs.ML Sun Jun 07 14:36:36 2015 +0200
+++ b/src/Pure/Isar/local_defs.ML Sun Jun 07 15:01:07 2015 +0200
@@ -96,7 +96,7 @@
ctxt
|> Proof_Context.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2
|> fold Variable.declare_term eqs
- |> Proof_Context.add_assms_i def_export (map2 (fn b => fn eq => (b, [(eq, [])])) bs eqs)
+ |> Proof_Context.add_assms def_export (map2 (fn b => fn eq => (b, [(eq, [])])) bs eqs)
|>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
end;