# HG changeset patch
# User wenzelm
# Date 1007595744 -3600
# Node ID 3e3bd3d449b5c32c5c7d6c6aa5d1ed4f6ffb6a30
# Parent  cef751fff6b096f229b6e18f2948de3acad87a15
tuned xtra_netpair;

diff -r cef751fff6b0 -r 3e3bd3d449b5 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Thu Dec 06 00:42:00 2001 +0100
+++ b/src/Provers/blast.ML	Thu Dec 06 00:42:24 2001 +0100
@@ -65,7 +65,7 @@
 		 swrappers: (string * wrapper) list, 
 		 uwrappers: (string * wrapper) list,
 		 safe0_netpair: netpair, safep_netpair: netpair,
-		 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair}
+		 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair}
   val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
   end;