diff -r 91d71bde1112 -r ac9d126456e1 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Mon Jun 04 15:43:32 2007 +0200
+++ b/src/Pure/goal.ML	Mon Jun 04 21:04:19 2007 +0200
@@ -37,6 +37,7 @@
   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;
 
 structure Goal: GOAL =
@@ -236,6 +237,18 @@
   | ([], _) => raise THM ("comp_hhf: no unifiers", 1, [tha, thb])
   | _  => raise THM ("comp_hhf: multiple unifiers", 1, [tha, thb]));
 
+
+(* non-atomic goal assumptions *)
+
+fun assume_rule_tac ctxt = norm_hhf_tac THEN' CSUBGOAL (fn (goal, i) =>
+  let
+    val ((_, goal'), ctxt') = Variable.focus goal ctxt;
+    val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
+    val Rs = filter_out (Logic.is_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
+    val tacs = Rs |> map (fn R =>
+      Tactic.etac (MetaSimplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac);
+  in fold_rev (curry op APPEND') tacs (K no_tac) i end);
+
 end;
 
 structure BasicGoal: BASIC_GOAL = Goal;