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);
```