--- 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;