src/Pure/theory.ML
changeset 19700 e02af528ceef
parent 19693 ab816ca8df06
child 19708 a508bde37a81
     1.1 --- a/src/Pure/theory.ML	Mon May 22 22:29:18 2006 +0200
     1.2 +++ b/src/Pure/theory.ML	Mon May 22 22:29:19 2006 +0200
     1.3 @@ -151,10 +151,16 @@
     1.4  val defs_of = #defs o rep_theory;
     1.5  
     1.6  fun definitions_of thy c =
     1.7 -  Defs.specifications_of (defs_of thy) c
     1.8 -  |> map_filter (fn (_, {is_def, module, name, lhs, rhs}) =>
     1.9 -    if is_def then SOME {module = module, name = name, lhs = lhs, rhs = rhs} else NONE);
    1.10 -
    1.11 +  let
    1.12 +    val inst = Consts.instance (Sign.consts_of thy);
    1.13 +    val defs = defs_of thy;
    1.14 +  in
    1.15 +    Defs.specifications_of defs c
    1.16 +    |> map_filter (fn (_, {is_def, module, name, lhs, rhs}) =>
    1.17 +      if is_def then SOME {module = module, name = name, lhs = inst (c, lhs),
    1.18 +        rhs = map (fn (d, Us) => (d, inst (d, Us))) rhs}
    1.19 +      else NONE)
    1.20 +  end;
    1.21  
    1.22  fun requires thy name what =
    1.23    if Context.exists_name name thy then ()