removed unused compose_hhf, comp_hhf;
authorwenzelm
Mon Nov 05 23:17:02 2007 +0100 (2007-11-05)
changeset 2530124e027f55f45
parent 25300 bc3a1c964704
child 25302 19b1729f1bd4
removed unused compose_hhf, comp_hhf;
src/Pure/goal.ML
     1.1 --- a/src/Pure/goal.ML	Mon Nov 05 22:53:38 2007 +0100
     1.2 +++ b/src/Pure/goal.ML	Mon Nov 05 23:17:02 2007 +0100
     1.3 @@ -33,9 +33,7 @@
     1.4    val precise_conjunction_tac: int -> int -> tactic
     1.5    val recover_conjunction_tac: tactic
     1.6    val norm_hhf_tac: int -> tactic
     1.7 -  val compose_hhf: thm -> int -> thm -> thm Seq.seq
     1.8    val compose_hhf_tac: thm -> int -> tactic
     1.9 -  val comp_hhf: thm -> thm -> thm
    1.10    val assume_rule_tac: Proof.context -> int -> tactic
    1.11  end;
    1.12  
    1.13 @@ -215,16 +213,8 @@
    1.14      if Drule.is_norm_hhf t then all_tac
    1.15      else MetaSimplifier.rewrite_goal_tac [Drule.norm_hhf_eq] i);
    1.16  
    1.17 -fun compose_hhf tha i thb =
    1.18 -  Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of thb i) tha, 0) i thb;
    1.19 -
    1.20 -fun compose_hhf_tac th i = PRIMSEQ (compose_hhf th i);
    1.21 -
    1.22 -fun comp_hhf tha thb =
    1.23 -  (case Seq.chop 2 (compose_hhf tha 1 thb) of
    1.24 -    ([th], _) => th
    1.25 -  | ([], _) => raise THM ("comp_hhf: no unifiers", 1, [tha, thb])
    1.26 -  | _  => raise THM ("comp_hhf: multiple unifiers", 1, [tha, thb]));
    1.27 +fun compose_hhf_tac th i st =
    1.28 +  PRIMSEQ (Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st;
    1.29  
    1.30  
    1.31  (* non-atomic goal assumptions *)