diff -r 1ecda5544e88 -r e02af528ceef src/Pure/theory.ML
--- a/src/Pure/theory.ML	Mon May 22 22:29:18 2006 +0200
+++ b/src/Pure/theory.ML	Mon May 22 22:29:19 2006 +0200
@@ -151,10 +151,16 @@
 val defs_of = #defs o rep_theory;
 
 fun definitions_of thy c =
-  Defs.specifications_of (defs_of thy) c
-  |> map_filter (fn (_, {is_def, module, name, lhs, rhs}) =>
-    if is_def then SOME {module = module, name = name, lhs = lhs, rhs = rhs} else NONE);
-
+  let
+    val inst = Consts.instance (Sign.consts_of thy);
+    val defs = defs_of thy;
+  in
+    Defs.specifications_of defs c
+    |> map_filter (fn (_, {is_def, module, name, lhs, rhs}) =>
+      if is_def then SOME {module = module, name = name, lhs = inst (c, lhs),
+        rhs = map (fn (d, Us) => (d, inst (d, Us))) rhs}
+      else NONE)
+  end;
 
 fun requires thy name what =
   if Context.exists_name name thy then ()