src/Pure/goal.ML
changeset 23356 dbe3731241c3
parent 23237 ac9d126456e1
child 23414 927203ad4b3a
     1.1 --- a/src/Pure/goal.ML	Wed Jun 13 00:01:58 2007 +0200
     1.2 +++ b/src/Pure/goal.ML	Wed Jun 13 00:01:59 2007 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4    val finish: thm -> thm
     1.5    val norm_result: thm -> thm
     1.6    val close_result: thm -> thm
     1.7 -  val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm
     1.8 +  val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
     1.9    val prove_multi: Proof.context -> string list -> term list -> term list ->
    1.10      ({prems: thm list, context: Proof.context} -> tactic) -> thm list
    1.11    val prove: Proof.context -> string list -> term list -> term ->
    1.12 @@ -103,9 +103,9 @@
    1.13  
    1.14  (** tactical theorem proving **)
    1.15  
    1.16 -(* prove_raw -- no checks, no normalization of result! *)
    1.17 +(* prove_internal -- minimal checks, no normalization of result! *)
    1.18  
    1.19 -fun prove_raw casms cprop tac =
    1.20 +fun prove_internal casms cprop tac =
    1.21    (case SINGLE (tac (map Assumption.assume casms)) (init cprop) of
    1.22      SOME th => Drule.implies_intr_list casms (finish th)
    1.23    | NONE => error "Tactic failed.");
    1.24 @@ -240,11 +240,15 @@
    1.25  
    1.26  (* non-atomic goal assumptions *)
    1.27  
    1.28 +fun non_atomic (Const ("==>", _) $ _ $ _) = true
    1.29 +  | non_atomic (Const ("all", _) $ _) = true
    1.30 +  | non_atomic _ = false;
    1.31 +
    1.32  fun assume_rule_tac ctxt = norm_hhf_tac THEN' CSUBGOAL (fn (goal, i) =>
    1.33    let
    1.34      val ((_, goal'), ctxt') = Variable.focus goal ctxt;
    1.35      val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
    1.36 -    val Rs = filter_out (Logic.is_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
    1.37 +    val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
    1.38      val tacs = Rs |> map (fn R =>
    1.39        Tactic.etac (MetaSimplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac);
    1.40    in fold_rev (curry op APPEND') tacs (K no_tac) i end);