# HG changeset patch
# User wenzelm
# Date 1129651175 -7200
# Node ID 7b35ce796a4d18bd38edffb8206a07496ce5a207
# Parent  75d3120779419d0e8e5abe2bbefeb0d38503a586
renamed atomize_rule to atomize_cterm;

diff -r 75d312077941 -r 7b35ce796a4d src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Tue Oct 18 17:59:34 2005 +0200
+++ b/src/Pure/Isar/object_logic.ML	Tue Oct 18 17:59:35 2005 +0200
@@ -17,8 +17,8 @@
   val declare_atomize: theory attribute
   val declare_rulify: theory attribute
   val atomize_term: theory -> term -> term
+  val atomize_cterm: theory -> cterm -> thm
   val atomize_thm: thm -> thm
-  val atomize_rule: theory -> cterm -> thm
   val atomize_tac: int -> tactic
   val full_atomize_tac: int -> tactic
   val atomize_goal: int -> thm -> thm
@@ -140,11 +140,8 @@
 fun atomize_term thy =
   drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) [];
 
-fun atomize_rule thy = Tactic.rewrite true (get_atomize thy);
-
-(*convert a natural-deduction rule into an object-level formula*)
-fun atomize_thm th =
-  rewrite_rule (get_atomize (Thm.theory_of_thm th)) th;
+fun atomize_cterm thy = Tactic.rewrite true (get_atomize thy);
+fun atomize_thm th = rewrite_rule (get_atomize (Thm.theory_of_thm th)) th;
 
 fun atomize_tac i st =
   if Logic.has_meta_prems (Thm.prop_of st) i then