# HG changeset patch
# User paulson
# Date 1084546117 -7200
# Node ID 81001d6cb8c0696bf8182df3b9ea22353dee5439
# Parent  dde816115d6ae8476a21294e25768a50c0ccc074
conversion of theorems to atomic form

diff -r dde816115d6a -r 81001d6cb8c0 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Thu May 13 16:02:29 2004 +0200
+++ b/src/Pure/Isar/object_logic.ML	Fri May 14 16:48:37 2004 +0200
@@ -18,6 +18,7 @@
   val declare_atomize: theory attribute
   val declare_rulify: theory attribute
   val atomize_term: Sign.sg -> term -> term
+  val atomize_thm: thm -> thm
   val atomize_rule: Sign.sg -> cterm -> thm
   val atomize_tac: int -> tactic
   val full_atomize_tac: int -> tactic
@@ -153,6 +154,10 @@
 
 fun atomize_rule sg = Tactic.rewrite true (get_atomize sg);
 
+(*Convert a natural-deduction rule into a formula (probably in FOL)*)
+fun atomize_thm th =
+  rewrite_rule  (get_atomize (Thm.sign_of_thm th)) th;
+
 fun atomize_tac i st =
   if Logic.has_meta_prems (Thm.prop_of st) i then
     (rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st