# HG changeset patch
# User wenzelm
# Date 949057439 -3600
# Node ID 7021549ef32d983aba28270042adc87ea4dc34a1
# Parent  941afb897532e51c73f51f4c9db514e91f89ca5a
map data;

diff -r 941afb897532 -r 7021549ef32d src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Fri Jan 28 11:23:41 2000 +0100
+++ b/src/Pure/Isar/calculation.ML	Fri Jan 28 12:03:59 2000 +0100
@@ -83,9 +83,6 @@
 
 local
 
-fun map_rules_global f thy = GlobalCalculation.put (f (GlobalCalculation.get thy)) thy;
-fun map_rules_local f ctxt = LocalCalculation.put (f (LocalCalculation.get ctxt)) ctxt;
-
 fun add_trans thm rules = Library.gen_ins Thm.eq_thm (thm, rules);
 fun del_trans thm rules = Library.gen_rem Thm.eq_thm (rules, thm);
 
@@ -93,10 +90,10 @@
 
 in
 
-val trans_add_global = mk_att map_rules_global add_trans;
-val trans_del_global = mk_att map_rules_global del_trans;
-val trans_add_local = mk_att map_rules_local (Library.apfst o add_trans);
-val trans_del_local = mk_att map_rules_local (Library.apfst o del_trans);
+val trans_add_global = mk_att GlobalCalculation.map add_trans;
+val trans_del_global = mk_att GlobalCalculation.map del_trans;
+val trans_add_local = mk_att LocalCalculation.map (Library.apfst o add_trans);
+val trans_del_local = mk_att LocalCalculation.map (Library.apfst o del_trans);
 
 end;