# HG changeset patch # User wenzelm # Date 1190579011 -7200 # Node ID 9d4982db07425a4a9b616ae2e2955a4779051fce # Parent 0d355aa59e67ea9e3f9996211718cb9dc2462993 tuned; diff -r 0d355aa59e67 -r 9d4982db0742 src/Pure/axclass.ML --- 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;