src/Pure/axclass.ML
changeset 24681 9d4982db0742
parent 24589 d3fca349736c
child 24712 64ed05609568
--- 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;