src/Pure/axclass.ML
changeset 24681 9d4982db0742
parent 24589 d3fca349736c
child 24712 64ed05609568
     1.1 --- a/src/Pure/axclass.ML	Sun Sep 23 22:23:27 2007 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sun Sep 23 22:23:31 2007 +0200
     1.3 @@ -305,9 +305,7 @@
     1.4        |> map_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
     1.5        |> Logic.close_form;
     1.6  
     1.7 -    (*FIXME is ProofContext.cert_propp really neccessary?*)
     1.8 -    val axiomss = ProofContext.cert_propp (ctxt, map (map (rpair []) o snd) raw_specs)
     1.9 -      |> snd |> map (map (prep_axiom o fst));
    1.10 +    val axiomss = map (map (prep_axiom o Sign.cert_prop thy) o snd) raw_specs;
    1.11      val name_atts = map fst raw_specs;
    1.12  
    1.13