src/Pure/theory.ML
changeset 19570 f199cb2295fd
parent 19482 9f11af8f7ef9
child 19592 856cd7460168
     1.1 --- a/src/Pure/theory.ML	Fri May 05 19:32:33 2006 +0200
     1.2 +++ b/src/Pure/theory.ML	Fri May 05 19:32:34 2006 +0200
     1.3 @@ -39,6 +39,8 @@
     1.4    val axioms_of: theory -> (string * term) list
     1.5    val all_axioms_of: theory -> (string * term) list
     1.6    val defs_of : theory -> Defs.T
     1.7 +  val definitions_of: theory -> string ->
     1.8 +    {module: string, name: string, lhs: typ, rhs: (string * typ) list} list
     1.9    val self_ref: theory -> theory_ref
    1.10    val deref: theory_ref -> theory
    1.11    val merge: theory * theory -> theory                     (*exception TERM*)
    1.12 @@ -148,6 +150,12 @@
    1.13  
    1.14  val defs_of = #defs o rep_theory;
    1.15  
    1.16 +fun definitions_of thy c =
    1.17 +  Defs.specifications_of (defs_of thy) c
    1.18 +  |> map_filter (fn (_, {is_def, module, name, lhs, rhs}) =>
    1.19 +    if is_def then SOME {module = module, name = name, lhs = lhs, rhs = rhs} else NONE);
    1.20 +
    1.21 +
    1.22  fun requires thy name what =
    1.23    if Context.exists_name name thy then ()
    1.24    else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
    1.25 @@ -258,9 +266,8 @@
    1.26      val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
    1.27      val _ = check_overloading thy overloaded lhs_const;
    1.28    in
    1.29 -    defs |> Defs.define (Sign.the_const_type thy)
    1.30 -      ((true, Context.theory_name thy), name) (prep_const thy lhs_const)
    1.31 -      (map (prep_const thy) rhs_consts)
    1.32 +    defs |> Defs.define (Sign.the_const_type thy) true (Context.theory_name thy)
    1.33 +      name (prep_const thy lhs_const) (map (prep_const thy) rhs_consts)
    1.34    end
    1.35    handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
    1.36     [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
    1.37 @@ -295,8 +302,8 @@
    1.38      fun const_of (Const const) = const
    1.39        | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
    1.40        | const_of _ = error "Attempt to finalize non-constant term";
    1.41 -    fun specify (c, T) = Defs.define (Sign.the_const_type thy)
    1.42 -      ((false, Context.theory_name thy), c ^ " axiom") (prep_const thy (c, T)) [];
    1.43 +    fun specify (c, T) = Defs.define (Sign.the_const_type thy) false (Context.theory_name thy)
    1.44 +      (c ^ " axiom") (prep_const thy (c, T)) [];
    1.45      val finalize = specify o check_overloading thy overloaded o
    1.46        const_of o Sign.no_vars (Sign.pp thy) o prep_term thy;
    1.47    in thy |> map_defs (fold finalize args) end;