src/Pure/axclass.ML
changeset 22745 17bc6af2011e
parent 22691 290454649b8c
child 22846 fb79144af9a3
     1.1 --- a/src/Pure/axclass.ML	Fri Apr 20 11:21:42 2007 +0200
     1.2 +++ b/src/Pure/axclass.ML	Fri Apr 20 11:21:47 2007 +0200
     1.3 @@ -21,11 +21,8 @@
     1.4    val add_arity: thm -> theory -> theory
     1.5    val prove_classrel: class * class -> tactic -> theory -> theory
     1.6    val prove_arity: string * sort list * sort -> tactic -> theory -> theory
     1.7 -  val define_class: bstring * xstring list -> string list ->
     1.8 -    ((bstring * Attrib.src list) * string list) list -> theory -> class * theory
     1.9 -  val define_class_i: bstring * class list -> string list ->
    1.10 +  val define_class: bstring * class list -> string list ->
    1.11      ((bstring * attribute list) * term list) list -> theory -> class * theory
    1.12 -  val read_param: theory -> string -> string
    1.13    val axiomatize_class: bstring * xstring list -> theory -> theory
    1.14    val axiomatize_class_i: bstring * class list -> theory -> theory
    1.15    val axiomatize_classrel: (xstring * xstring) list -> theory -> theory
    1.16 @@ -270,18 +267,7 @@
    1.17  
    1.18  (** class definitions **)
    1.19  
    1.20 -fun read_param thy raw_t =
    1.21 -  let
    1.22 -    val t = Sign.read_term thy raw_t
    1.23 -  in case try dest_Const t
    1.24 -   of SOME (c, _) => c
    1.25 -    | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
    1.26 -  end;
    1.27 -
    1.28 -local
    1.29 -
    1.30 -fun def_class prep_class prep_att prep_param prep_propp
    1.31 -    (bclass, raw_super) raw_params raw_specs thy =
    1.32 +fun define_class (bclass, raw_super) params raw_specs thy =
    1.33    let
    1.34      val ctxt = ProofContext.init thy;
    1.35      val pp = ProofContext.pp ctxt;
    1.36 @@ -291,7 +277,7 @@
    1.37  
    1.38      val bconst = Logic.const_of_class bclass;
    1.39      val class = Sign.full_name thy bclass;
    1.40 -    val super = map (prep_class thy) raw_super |> Sign.certify_sort thy;
    1.41 +    val super = Sign.certify_sort thy raw_super;
    1.42  
    1.43      fun prep_axiom t =
    1.44        (case Term.add_tfrees t [] of
    1.45 @@ -305,9 +291,10 @@
    1.46        |> map_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
    1.47        |> Logic.close_form;
    1.48  
    1.49 -    val axiomss = prep_propp (ctxt, map (map (rpair []) o snd) raw_specs)
    1.50 +    (*FIXME is ProofContext.cert_propp really neccessary?*)
    1.51 +    val axiomss = ProofContext.cert_propp (ctxt, map (map (rpair []) o snd) raw_specs)
    1.52        |> snd |> map (map (prep_axiom o fst));
    1.53 -    val name_atts = Attrib.map_specs (prep_att thy) raw_specs |> map fst;
    1.54 +    val name_atts = map fst raw_specs;
    1.55  
    1.56  
    1.57      (* definition *)
    1.58 @@ -336,7 +323,6 @@
    1.59  
    1.60      (* params *)
    1.61  
    1.62 -    val params = map (prep_param thy) raw_params;
    1.63      val params_typs = map (fn param =>
    1.64        let
    1.65          val ty = Sign.the_const_type thy param;
    1.66 @@ -361,13 +347,6 @@
    1.67  
    1.68    in (class, result_thy) end;
    1.69  
    1.70 -in
    1.71 -
    1.72 -val define_class = def_class Sign.read_class Attrib.attribute read_param ProofContext.read_propp;
    1.73 -val define_class_i = def_class Sign.certify_class (K I) (K I) ProofContext.cert_propp;
    1.74 -
    1.75 -end;
    1.76 -
    1.77  
    1.78  
    1.79  (** axiomatizations **)