--- a/src/HOL/Tools/inductive.ML Sat Apr 16 12:46:18 2011 +0200
+++ b/src/HOL/Tools/inductive.ML Sat Apr 16 13:48:45 2011 +0200
@@ -151,7 +151,7 @@
val (tab, monos) = get_inductives ctxt;
val space = Consts.space_of (ProofContext.consts_of ctxt);
in
- [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table (space, tab))),
+ [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table ctxt (space, tab))),
Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
|> Pretty.chunks |> Pretty.writeln
end;