# HG changeset patch
# User wenzelm
# Date 1194301022 -3600
# Node ID 24e027f55f45d01f6343ed1c9e9a31925a7d3eff
# Parent  bc3a1c9647044026be111934b416a083aa09229c
removed unused compose_hhf, comp_hhf;

diff -r bc3a1c964704 -r 24e027f55f45 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Mon Nov 05 22:53:38 2007 +0100
+++ b/src/Pure/goal.ML	Mon Nov 05 23:17:02 2007 +0100
@@ -33,9 +33,7 @@
   val precise_conjunction_tac: int -> int -> tactic
   val recover_conjunction_tac: tactic
   val norm_hhf_tac: int -> tactic
-  val compose_hhf: thm -> int -> thm -> thm Seq.seq
   val compose_hhf_tac: thm -> int -> tactic
-  val comp_hhf: thm -> thm -> thm
   val assume_rule_tac: Proof.context -> int -> tactic
 end;
 
@@ -215,16 +213,8 @@
     if Drule.is_norm_hhf t then all_tac
     else MetaSimplifier.rewrite_goal_tac [Drule.norm_hhf_eq] i);
 
-fun compose_hhf tha i thb =
-  Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of thb i) tha, 0) i thb;
-
-fun compose_hhf_tac th i = PRIMSEQ (compose_hhf th i);
-
-fun comp_hhf tha thb =
-  (case Seq.chop 2 (compose_hhf tha 1 thb) of
-    ([th], _) => th
-  | ([], _) => raise THM ("comp_hhf: no unifiers", 1, [tha, thb])
-  | _  => raise THM ("comp_hhf: multiple unifiers", 1, [tha, thb]));
+fun compose_hhf_tac th i st =
+  PRIMSEQ (Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st;
 
 
 (* non-atomic goal assumptions *)