# HG changeset patch
# User wenzelm
# Date 965082012 -7200
# Node ID 3bda55143260f6631f5f3ec570f4183b80f8d21a
# Parent  708a8a05497dc851e148ab9dde9528c53a50891a
(un)fold: CHANGED;
added atomize_tac;

diff -r 708a8a05497d -r 3bda55143260 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Aug 01 00:19:07 2000 +0200
+++ b/src/Pure/Isar/method.ML	Tue Aug 01 00:20:12 2000 +0200
@@ -38,6 +38,7 @@
   val insert_facts: Proof.method
   val unfold: thm list -> Proof.method
   val fold: thm list -> Proof.method
+  val atomize_tac: thm list -> int -> tactic
   val multi_resolve: thm list -> thm -> thm Seq.seq
   val multi_resolves: thm list -> thm list -> thm Seq.seq
   val resolveq_tac: thm Seq.seq -> int -> tactic
@@ -242,8 +243,20 @@
 
 (* unfold / fold definitions *)
 
-fun unfold thms = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN rewrite_goals_tac thms);
-fun fold thms = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN fold_goals_tac thms);
+fun unfold thms = METHOD (fn facts =>
+  ALLGOALS (insert_tac facts) THEN CHANGED (rewrite_goals_tac thms));
+
+fun fold thms = METHOD (fn facts =>
+  ALLGOALS (insert_tac facts) THEN CHANGED (fold_goals_tac thms));
+
+
+(* atomize meta-connectives *)
+
+fun atomize_tac rews i st =
+  if Logic.has_meta_prems (#prop (Thm.rep_thm st)) i then
+    (warning "FIXME: atomize_tac";
+    Tactic.asm_rewrite_goal_tac (true, false, false) (K no_tac) (Thm.mss_of rews) i st)
+  else all_tac st;
 
 
 (* multi_resolve *)