# HG changeset patch
# User wenzelm
# Date 1160353205 -7200
# Node ID 380663e636a8fb89b4daa4e24b6295d311a684f9
# Parent  8fc5850446ed69c58a254d0b47c379d1a8f68c9e
attribute: Context.mapping;
removed Drule.strip_shyps_warning;

diff -r 8fc5850446ed -r 380663e636a8 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Mon Oct 09 02:20:04 2006 +0200
+++ b/src/Pure/Isar/object_logic.ML	Mon Oct 09 02:20:05 2006 +0200
@@ -136,13 +136,11 @@
 val get_atomize = #1 o #2 o ObjectLogicData.get;
 val get_rulify = #2 o #2 o ObjectLogicData.get;
 
-val declare_atomize =
-  Thm.declaration_attribute (Context.map_theory o ObjectLogicData.map o
-    Library.apsnd o Library.apfst o Drule.add_rule);
+val declare_atomize = Thm.declaration_attribute (fn th =>
+  Context.mapping (ObjectLogicData.map (apsnd (apfst (Drule.add_rule th)))) I);
 
-val declare_rulify =
-  Thm.declaration_attribute (Context.map_theory o ObjectLogicData.map o
-    Library.apsnd o Library.apsnd o Drule.add_rule);
+val declare_rulify = Thm.declaration_attribute (fn th =>
+  Context.mapping (ObjectLogicData.map (apsnd (apsnd (Drule.add_rule th)))) I);
 
 
 (* atomize *)
@@ -177,7 +175,7 @@
 
 fun gen_rulify full thm =
   Tactic.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
-  |> Drule.gen_all |> Drule.strip_shyps_warning |> Drule.zero_var_indexes;
+  |> Drule.gen_all |> Thm.strip_shyps |> Drule.zero_var_indexes;
 
 val rulify = gen_rulify true;
 val rulify_no_asm = gen_rulify false;