# HG changeset patch
# User wenzelm
# Date 1255792739 -7200
# Node ID 55ba9b6648efca041997275ff43d49980722edda
# Parent  fbd2bb2489a84bd200025d48dbdc5c169e6b4b69
less pervasive names;

diff -r fbd2bb2489a8 -r 55ba9b6648ef src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Sat Oct 17 16:58:03 2009 +0200
+++ b/src/Pure/tactic.ML	Sat Oct 17 17:18:59 2009 +0200
@@ -46,7 +46,6 @@
     int -> tactic
   val net_biresolve_tac: (bool * thm) list -> int -> tactic
   val net_bimatch_tac: (bool * thm) list -> int -> tactic
-  val build_net: thm list -> (int * thm) Net.net
   val filt_resolve_tac: thm list -> int -> int -> tactic
   val resolve_from_net_tac: (int * thm) Net.net -> int -> tactic
   val match_from_net_tac: (int * thm) Net.net -> int -> tactic
@@ -75,6 +74,7 @@
     ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
       ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
   val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) -> bool
+  val build_net: thm list -> (int * thm) Net.net
 end;
 
 structure Tactic: TACTIC =
@@ -385,5 +385,5 @@
 
 end;
 
-structure BasicTactic: BASIC_TACTIC = Tactic;
-open BasicTactic;
+structure Basic_Tactic: BASIC_TACTIC = Tactic;
+open Basic_Tactic;