src/Pure/tactic.ML
changeset 2672 85d7e800d754
parent 2580 e3f680709487
child 2688 889a1cbd1aca
     1.1 --- a/src/Pure/tactic.ML	Fri Feb 21 15:30:41 1997 +0100
     1.2 +++ b/src/Pure/tactic.ML	Fri Feb 21 15:31:47 1997 +0100
     1.3 @@ -61,6 +61,7 @@
     1.4    val net_biresolve_tac: (bool*thm) list -> int -> tactic
     1.5    val net_match_tac: thm list -> int -> tactic
     1.6    val net_resolve_tac: thm list -> int -> tactic
     1.7 +  val orderlist: (int * 'a) list -> 'a list
     1.8    val PRIMITIVE: (thm -> thm) -> tactic  
     1.9    val PRIMSEQ: (thm -> thm Sequence.seq) -> tactic  
    1.10    val prune_params_tac: tactic
    1.11 @@ -387,7 +388,7 @@
    1.12        let val hyps = Logic.strip_assums_hyp prem
    1.13            and concl = Logic.strip_assums_concl prem 
    1.14            val kbrls = Net.unify_term inet concl @
    1.15 -                      flat (map (Net.unify_term enet) hyps)
    1.16 +                      List.concat (map (Net.unify_term enet) hyps)
    1.17        in PRIMSEQ (biresolution match (orderlist kbrls) i) end);
    1.18  
    1.19  (*versions taking pre-built nets*)
    1.20 @@ -527,11 +528,8 @@
    1.21  
    1.22  (*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
    1.23    right to left if n is positive, and from left to right if n is negative.*)
    1.24 -fun rotate_tac n =
    1.25 -  let fun rot(n) = EVERY'(replicate n (dtac asm_rl));
    1.26 -  in if n >= 0 then rot n
    1.27 -     else SUBGOAL (fn (t,i) => rot(length(Logic.strip_assums_hyp t)+n) i)
    1.28 -  end;
    1.29 +fun rotate_tac 0 i = all_tac
    1.30 +  | rotate_tac k i = PRIMITIVE (rotate_rule k i);
    1.31  
    1.32  end;
    1.33