Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Sun, 23 Sep 2007 22:23:31 +0200
changeset 24681 9d4982db0742
parent 24680 0d355aa59e67
child 24682 29306b20079b
tuned;
src/Pure/axclass.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle