src/Pure/Isar/method.ML
changeset 11765 4c45eb23ef68
parent 11731 1a0c1ef86518
child 11785 3087d6f19adc
     1.1 --- a/src/Pure/Isar/method.ML	Sun Oct 14 20:09:19 2001 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Sun Oct 14 20:09:59 2001 +0200
     1.3 @@ -41,9 +41,6 @@
     1.4    val insert_facts: Proof.method
     1.5    val unfold: thm list -> Proof.method
     1.6    val fold: thm list -> Proof.method
     1.7 -  val atomize_tac: thm list -> int -> tactic
     1.8 -  val atomize_goal: thm list -> int -> thm -> thm
     1.9 -  val atomize_strip_tac: thm list * thm list -> int -> tactic
    1.10    val multi_resolve: thm list -> thm -> thm Seq.seq
    1.11    val multi_resolves: thm list -> thm list -> thm Seq.seq
    1.12    val rule_tac: thm list -> thm list -> int -> tactic
    1.13 @@ -284,23 +281,6 @@
    1.14  fun fold thms = SIMPLE_METHOD (CHANGED_PROP (fold_goals_tac thms));
    1.15  
    1.16  
    1.17 -(* atomize meta-connectives *)
    1.18 -
    1.19 -fun atomize_strip_tac (rews, strip) =
    1.20 -  let val rew_tac = rewrite_goal_tac rews in
    1.21 -    fn i => fn thm =>
    1.22 -      if Logic.has_meta_prems (#prop (Thm.rep_thm thm)) i then
    1.23 -        (rew_tac i THEN REPEAT (match_tac strip i)) thm
    1.24 -      else all_tac thm
    1.25 -  end;
    1.26 -
    1.27 -fun atomize_tac rews = atomize_strip_tac (rews, []);
    1.28 -
    1.29 -fun atomize_goal rews =
    1.30 -  let val tac = atomize_tac rews
    1.31 -  in fn i => fn thm => (case Seq.pull (tac i thm) of None => thm | Some (thm', _) => thm') end;
    1.32 -
    1.33 -
    1.34  (* multi_resolve *)
    1.35  
    1.36  local