# HG changeset patch
# User boehmes
# Date 1320758964 -3600
# Node ID d58c25559dc00747840d9dafcd0bb6073106ca4b
# Parent  5abb0e738b00f48ffcfc63613e4ae1a208650d91
made SML/NJ happy

diff -r 5abb0e738b00 -r d58c25559dc0 src/HOL/Tools/SMT/z3_proof_tools.ML
--- 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