# HG changeset patch
# User wenzelm
# Date 1138144901 -3600
# Node ID 628e5761053603977cc171078f98ae9e5bcb495c
# Parent  e4d9d718b8bb581d220d94543cffb193d3ccccce
tuned atomize_cterm;
added reverse_atomize_term/tac;

diff -r e4d9d718b8bb -r 628e57610536 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Wed Jan 25 00:21:40 2006 +0100
+++ b/src/Pure/Isar/object_logic.ML	Wed Jan 25 00:21:41 2006 +0100
@@ -17,11 +17,13 @@
   val declare_atomize: attribute
   val declare_rulify: attribute
   val atomize_term: theory -> term -> term
-  val atomize_cterm: theory -> cterm -> thm
+  val atomize_cterm: cterm -> thm
   val atomize_thm: thm -> thm
   val atomize_tac: int -> tactic
   val full_atomize_tac: int -> tactic
   val atomize_goal: int -> thm -> thm
+  val reverse_atomize_term: theory -> term -> term
+  val reverse_atomize_tac: int -> tactic
   val rulify: thm -> thm
   val rulify_no_asm: thm -> thm
   val rule_format: attribute
@@ -121,6 +123,7 @@
 (* maintain rules *)
 
 val get_atomize = #1 o #2 o ObjectLogicData.get;
+val get_reverse_atomize = map Thm.symmetric o get_atomize;
 val get_rulify = #2 o #2 o ObjectLogicData.get;
 
 val declare_atomize =
@@ -142,7 +145,7 @@
 fun atomize_term thy =
   drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) [];
 
-fun atomize_cterm thy = Tactic.rewrite true (get_atomize thy);
+fun atomize_cterm ct = Tactic.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
 fun atomize_thm th = rewrite_rule (get_atomize (Thm.theory_of_thm th)) th;
 
 fun atomize_tac i st =
@@ -157,6 +160,12 @@
   (case Seq.pull (atomize_tac i st) of NONE => st | SOME (st', _) => st');
 
 
+(* reverse atomize -- not necessarily the same as rulify! *)
+
+fun reverse_atomize_term thy = MetaSimplifier.rewrite_term thy (get_reverse_atomize thy) [];
+fun reverse_atomize_tac i st = rewrite_goal_tac (get_reverse_atomize (Thm.theory_of_thm st)) i st;
+
+
 (* rulify *)
 
 fun gen_rulify full thm =