equal
deleted
inserted
replaced
1382 (data, keys) |
1382 (data, keys) |
1383 end; |
1383 end; |
1384 |
1384 |
1385 fun add_equations name thy = |
1385 fun add_equations name thy = |
1386 let |
1386 let |
1387 val thy' = PredData.map (Graph.extend (dependencies_of thy) [name]) thy; |
1387 val thy' = PredData.map (Graph.extend (dependencies_of thy) name) thy; |
1388 (*val preds = Graph.all_preds (PredData.get thy') [name] |> filter_out (has_elim thy') *) |
1388 (*val preds = Graph.all_preds (PredData.get thy') [name] |> filter_out (has_elim thy') *) |
1389 fun strong_conn_of gr keys = |
1389 fun strong_conn_of gr keys = |
1390 Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr) |
1390 Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr) |
1391 val scc = strong_conn_of (PredData.get thy') [name] |
1391 val scc = strong_conn_of (PredData.get thy') [name] |
1392 val thy'' = fold_rev |
1392 val thy'' = fold_rev |
1411 fun generic_code_pred prep_const raw_const lthy = |
1411 fun generic_code_pred prep_const raw_const lthy = |
1412 let |
1412 let |
1413 val thy = (ProofContext.theory_of lthy) |
1413 val thy = (ProofContext.theory_of lthy) |
1414 val const = prep_const thy raw_const |
1414 val const = prep_const thy raw_const |
1415 val lthy' = lthy |
1415 val lthy' = lthy |
1416 val thy' = PredData.map (Graph.extend (dependencies_of thy) [const]) thy |
1416 val thy' = PredData.map (Graph.extend (dependencies_of thy) const) thy |
1417 val preds = Graph.all_preds (PredData.get thy') [const] |> filter_out (has_elim thy') |
1417 val preds = Graph.all_preds (PredData.get thy') [const] |> filter_out (has_elim thy') |
1418 val _ = Output.tracing ("preds: " ^ commas preds) |
1418 val _ = Output.tracing ("preds: " ^ commas preds) |
1419 (* |
1419 (* |
1420 fun mk_elim pred = |
1420 fun mk_elim pred = |
1421 let |
1421 let |