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.
simplified Graph.extend;
authorwenzelm
Wed, 10 Jun 2009 00:46:37 +0200
changeset 31541 4ed9d9dc17ee
parent 31540 4cfe0f756feb
child 31542 3371a3c19bb1
child 31549 f7379ea2c949
child 31601 55644fd600c7
simplified Graph.extend;
src/HOL/ex/predicate_compile.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/ex/predicate_compile.ML	Wed Jun 10 00:46:15 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Wed Jun 10 00:46:37 2009 +0200
@@ -1384,7 +1384,7 @@
 
 fun add_equations name thy =
   let
-    val thy' = PredData.map (Graph.extend (dependencies_of thy) [name]) thy;
+    val thy' = PredData.map (Graph.extend (dependencies_of thy) name) thy;
     (*val preds = Graph.all_preds (PredData.get thy') [name] |> filter_out (has_elim thy') *)
     fun strong_conn_of gr keys =
       Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
@@ -1413,7 +1413,7 @@
     val thy = (ProofContext.theory_of lthy)
     val const = prep_const thy raw_const
     val lthy' = lthy
-    val thy' = PredData.map (Graph.extend (dependencies_of thy) [const]) thy
+    val thy' = PredData.map (Graph.extend (dependencies_of thy) const) thy
     val preds = Graph.all_preds (PredData.get thy') [const] |> filter_out (has_elim thy')
     val _ = Output.tracing ("preds: " ^ commas preds)
     (*
isabelle