diff -r c5146d5fc54c -r dda4aef7cba4 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sat May 14 22:00:24 2011 +0200
+++ b/src/Provers/blast.ML	Sun May 15 16:40:24 2011 +0200
@@ -35,9 +35,6 @@
         "no DETERM" flag would prevent proofs failing here.
 *)
 
-(*Should be a type abbreviation?*)
-type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;
-
 signature BLAST_DATA =
 sig
   structure Classical: CLASSICAL
@@ -554,7 +551,7 @@
   | toTerm d (f $ u)       = Term.$ (toTerm d f, toTerm (d-1) u);
 
 
-fun netMkRules ctxt P vars (nps: netpair list) =
+fun netMkRules ctxt P vars (nps: Classical.netpair list) =
   case P of
       (Const ("*Goal*", _) $ G) =>
         let val pG = mk_Trueprop (toTerm 2 G)