--- a/src/HOL/Tools/recdef_package.ML Sat Jun 11 22:15:47 2005 +0200
+++ b/src/HOL/Tools/recdef_package.ML Sat Jun 11 22:15:48 2005 +0200
@@ -120,8 +120,8 @@
Drule.merge_rules (wfs1, wfs2)));
fun print sg (tab, hints) =
- (Pretty.strs ("recdefs:" :: map #1 (Sign.extern_table sg Sign.constK tab)) ::
- pretty_hints hints) |> Pretty.chunks |> Pretty.writeln;
+ (Pretty.strs ("recdefs:" :: map #1 (NameSpace.extern_table (Sign.const_space sg, tab))) ::
+ pretty_hints hints) |> Pretty.chunks |> Pretty.writeln;
end;
structure GlobalRecdefData = TheoryDataFun(GlobalRecdefArgs);