# HG changeset patch
# User wenzelm
# Date 1181685719 -7200
# Node ID dbe3731241c3cbfc851ad207654ff3f447bcda67
# Parent  d2c033fd4514cbf81723b25c07ccd833cb5a4a1d
renamed prove_raw to prove_internal;
tuned;

diff -r d2c033fd4514 -r dbe3731241c3 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Jun 13 00:01:58 2007 +0200
+++ b/src/Pure/goal.ML	Wed Jun 13 00:01:59 2007 +0200
@@ -21,7 +21,7 @@
   val finish: thm -> thm
   val norm_result: thm -> thm
   val close_result: thm -> thm
-  val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm
+  val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
   val prove_multi: Proof.context -> string list -> term list -> term list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm list
   val prove: Proof.context -> string list -> term list -> term ->
@@ -103,9 +103,9 @@
 
 (** tactical theorem proving **)
 
-(* prove_raw -- no checks, no normalization of result! *)
+(* prove_internal -- minimal checks, no normalization of result! *)
 
-fun prove_raw casms cprop tac =
+fun prove_internal casms cprop tac =
   (case SINGLE (tac (map Assumption.assume casms)) (init cprop) of
     SOME th => Drule.implies_intr_list casms (finish th)
   | NONE => error "Tactic failed.");
@@ -240,11 +240,15 @@
 
 (* non-atomic goal assumptions *)
 
+fun non_atomic (Const ("==>", _) $ _ $ _) = true
+  | non_atomic (Const ("all", _) $ _) = true
+  | non_atomic _ = false;
+
 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 Rs = filter (non_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);