author | boehmes |
Tue, 08 Nov 2011 14:29:24 +0100 | |
changeset 45410 | d58c25559dc0 |
parent 45409 | 5abb0e738b00 |
child 45411 | af607f4945f4 |
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Tue Nov 08 10:48:58 2011 +0100 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Tue Nov 08 14:29:24 2011 +0100 @@ -74,10 +74,11 @@ in (case select ct of [] => select' ct | xthms' => xthms') end in -val net_instances = +fun net_instances net = instances_from_net false (fn f => fn (i, thm) => Option.map (pair i) (f thm)) + net -val net_instance = try hd oo instances_from_net true I +fun net_instance net = try hd o instances_from_net true I net end