src/Pure/tactic.ML
changeset 670 ff4c6691de9d
parent 439 ad3f46c13f1e
child 761 04320c295500
     1.1 --- a/src/Pure/tactic.ML	Mon Oct 31 17:59:49 1994 +0100
     1.2 +++ b/src/Pure/tactic.ML	Mon Oct 31 18:01:02 1994 +0100
     1.3 @@ -16,12 +16,15 @@
     1.4          bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
     1.5    val assume_tac: int -> tactic
     1.6    val atac: int ->tactic
     1.7 -  val bimatch_from_nets_tac: (int*(bool*thm)) net * (int*(bool*thm)) net -> int -> tactic
     1.8 +  val bimatch_from_nets_tac: 
     1.9 +      (int*(bool*thm)) net * (int*(bool*thm)) net -> int -> tactic
    1.10    val bimatch_tac: (bool*thm)list -> int -> tactic
    1.11 -  val biresolve_from_nets_tac: (int*(bool*thm)) net * (int*(bool*thm)) net -> int -> tactic
    1.12 +  val biresolve_from_nets_tac: 
    1.13 +      (int*(bool*thm)) net * (int*(bool*thm)) net -> int -> tactic
    1.14    val biresolve_tac: (bool*thm)list -> int -> tactic
    1.15    val build_net: thm list -> (int*thm) net
    1.16 -  val build_netpair: (bool*thm)list -> (int*(bool*thm)) net * (int*(bool*thm)) net
    1.17 +  val build_netpair:    (int*(bool*thm)) net * (int*(bool*thm)) net ->
    1.18 +      (bool*thm)list -> (int*(bool*thm)) net * (int*(bool*thm)) net
    1.19    val compose_inst_tac: (string*string)list -> (bool*thm*int) -> int -> tactic
    1.20    val compose_tac: (bool * thm * int) -> int -> tactic 
    1.21    val cut_facts_tac: thm list -> int -> tactic
    1.22 @@ -308,8 +311,8 @@
    1.23      else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet);
    1.24  
    1.25  (*build a pair of nets for biresolution*)
    1.26 -fun build_netpair brls = 
    1.27 -    foldr insert_kbrl (taglist 1 brls, (Net.empty,Net.empty));
    1.28 +fun build_netpair netpair brls = 
    1.29 +    foldr insert_kbrl (taglist 1 brls, netpair);
    1.30  
    1.31  (*biresolution using a pair of nets rather than rules*)
    1.32  fun biresolution_from_nets_tac match (inet,enet) =
    1.33 @@ -326,8 +329,11 @@
    1.34  val bimatch_from_nets_tac = biresolution_from_nets_tac true;
    1.35  
    1.36  (*fast versions using nets internally*)
    1.37 -val net_biresolve_tac = biresolve_from_nets_tac o build_netpair;
    1.38 -val net_bimatch_tac = bimatch_from_nets_tac o build_netpair;
    1.39 +val net_biresolve_tac =
    1.40 +    biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty);
    1.41 +
    1.42 +val net_bimatch_tac =
    1.43 +    bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty);
    1.44  
    1.45  (*** Simpler version for resolve_tac -- only one net, and no hyps ***)
    1.46