# HG changeset patch
# User wenzelm
# Date 1183658488 -7200
# Node ID d32a85385e177a418a7704874e5c42893ef8ee6c
# Parent  ad95084a5c63b6c9f0dd3c2b1fee030dea7bc9ac
simplified ObjectLogic.atomize;

diff -r ad95084a5c63 -r d32a85385e17 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Thu Jul 05 20:01:26 2007 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Thu Jul 05 20:01:28 2007 +0200
@@ -336,7 +336,7 @@
       | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
       | find_var _ = NONE;
     fun find_thm th =
-      let val th' = ObjectLogic.atomize_thm th
+      let val th' = Conv.fconv_rule ObjectLogic.atomize th
       in Option.map (pair (th, th')) (find_var (prop_of th')) end
   in
     case get_first find_thm thms of
diff -r ad95084a5c63 -r d32a85385e17 src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Thu Jul 05 20:01:26 2007 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML	Thu Jul 05 20:01:28 2007 +0200
@@ -88,7 +88,7 @@
     val cert = Thm.cterm_of thy;
 
     val ((insts, defs), defs_ctxt) = fold_map InductMethod.add_defs def_insts ctxt |>> split_list;
-    val atomized_defs = map (map ObjectLogic.atomize_thm) defs;
+    val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
 
     val finish_rule =
       split_all_tuples
diff -r ad95084a5c63 -r d32a85385e17 src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Thu Jul 05 20:01:26 2007 +0200
+++ b/src/HOL/Tools/specification_package.ML	Thu Jul 05 20:01:28 2007 +0200
@@ -121,7 +121,7 @@
           | myfoldr f [] = error "SpecificationPackage.process_spec internal error"
 
         val rew_imps = alt_props |>
-          map (ObjectLogic.atomize_cterm o Thm.read_cterm thy o rpair Term.propT o snd)
+          map (ObjectLogic.atomize o Thm.read_cterm thy o rpair Term.propT o snd)
         val props' = rew_imps |>
           map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of)
 
diff -r ad95084a5c63 -r d32a85385e17 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Thu Jul 05 20:01:26 2007 +0200
+++ b/src/Provers/blast.ML	Thu Jul 05 20:01:28 2007 +0200
@@ -1247,7 +1247,7 @@
         (also prints reconstruction time)
  "lim" is depth limit.*)
 fun timing_depth_tac start cs lim i st0 =
-  let val st = (initialize (theory_of_thm st0); ObjectLogic.atomize_goal i st0);
+  let val st = (initialize (theory_of_thm st0); Conv.gconv_rule ObjectLogic.atomize_prems i st0);
       val sign = Thm.theory_of_thm st
       val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
       val hyps  = strip_imp_prems skoprem
diff -r ad95084a5c63 -r d32a85385e17 src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Thu Jul 05 20:01:26 2007 +0200
+++ b/src/Provers/induct_method.ML	Thu Jul 05 20:01:28 2007 +0200
@@ -363,7 +363,7 @@
     val cert = Thm.cterm_of thy;
 
     val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
-    val atomized_defs = map (map ObjectLogic.atomize_thm) defs;
+    val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
 
     fun inst_rule (concls, r) =
       (if null insts then `RuleCases.get r
diff -r ad95084a5c63 -r d32a85385e17 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Jul 05 20:01:26 2007 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Jul 05 20:01:28 2007 +0200
@@ -1692,7 +1692,7 @@
     val bodyT = Term.fastype_of body;
   in
     if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
-    else (body, bodyT, ObjectLogic.atomize_cterm (Thm.cterm_of thy t))
+    else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t))
   end;
 
 fun aprop_tr' n c = (c, fn args =>