src/Pure/theory.ML
changeset 19700 e02af528ceef
parent 19693 ab816ca8df06
child 19708 a508bde37a81
equal deleted inserted replaced
19699:1ecda5544e88 19700:e02af528ceef
   149 fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy);
   149 fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy);
   150 
   150 
   151 val defs_of = #defs o rep_theory;
   151 val defs_of = #defs o rep_theory;
   152 
   152 
   153 fun definitions_of thy c =
   153 fun definitions_of thy c =
   154   Defs.specifications_of (defs_of thy) c
   154   let
   155   |> map_filter (fn (_, {is_def, module, name, lhs, rhs}) =>
   155     val inst = Consts.instance (Sign.consts_of thy);
   156     if is_def then SOME {module = module, name = name, lhs = lhs, rhs = rhs} else NONE);
   156     val defs = defs_of thy;
   157 
   157   in
       
   158     Defs.specifications_of defs c
       
   159     |> map_filter (fn (_, {is_def, module, name, lhs, rhs}) =>
       
   160       if is_def then SOME {module = module, name = name, lhs = inst (c, lhs),
       
   161         rhs = map (fn (d, Us) => (d, inst (d, Us))) rhs}
       
   162       else NONE)
       
   163   end;
   158 
   164 
   159 fun requires thy name what =
   165 fun requires thy name what =
   160   if Context.exists_name name thy then ()
   166   if Context.exists_name name thy then ()
   161   else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
   167   else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
   162 
   168