# HG changeset patch
# User wenzelm
# Date 1148329759 -7200
# Node ID e02af528ceef6d34dd6cacea0305ea7355846a9c
# Parent  1ecda5544e883a54040eff5541e2787741f01d76
Defs.specifications_of: lhs/rhs now use typargs;

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 ()