--- a/src/Pure/axclass.ML Sun Sep 23 22:23:27 2007 +0200
+++ b/src/Pure/axclass.ML Sun Sep 23 22:23:31 2007 +0200
@@ -305,9 +305,7 @@
|> map_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
|> Logic.close_form;
- (*FIXME is ProofContext.cert_propp really neccessary?*)
- val axiomss = ProofContext.cert_propp (ctxt, map (map (rpair []) o snd) raw_specs)
- |> snd |> map (map (prep_axiom o fst));
+ val axiomss = map (map (prep_axiom o Sign.cert_prop thy) o snd) raw_specs;
val name_atts = map fst raw_specs;