# HG changeset patch
# User wenzelm
# Date 1213808097 -7200
# Node ID 7eef2b1830324c3c1164645ced8334d522cc297a
# Parent  f339dc43ce9f12c5e1ac8dcd662860d1172d0679
simplified Abel_Cancel setup;

diff -r f339dc43ce9f -r 7eef2b183032 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Wed Jun 18 16:55:44 2008 +0200
+++ b/src/HOL/OrderedGroup.thy	Wed Jun 18 18:54:57 2008 +0200
@@ -1372,8 +1372,8 @@
 lemmas diff_le_0_iff_le [simp] = le_iff_diff_le_0 [symmetric]
 
 ML {*
-structure ab_group_add_cancel = Abel_Cancel(
-struct
+structure ab_group_add_cancel = Abel_Cancel
+(
 
 (* term order for abelian groups *)
 
@@ -1400,25 +1400,25 @@
     "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
 end;
 
+val eq_reflection = @{thm eq_reflection};
+  
+val T = @{typ "'a::ab_group_add"};
+
 val cancel_ss = HOL_basic_ss settermless termless_agrp
   addsimprocs [add_ac_proc] addsimps
   [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_def},
    @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
    @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
    @{thm minus_add_cancel}];
-  
-val eq_reflection = @{thm eq_reflection};
+
+val sum_pats = [@{cterm "x + y::'a::ab_group_add"}, @{cterm "x - y::'a::ab_group_add"}];
   
-val thy_ref = Theory.check_thy @{theory};
-
-val T = @{typ "'a\<Colon>ab_group_add"};
-
 val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}];
 
 val dest_eqI = 
   fst o HOLogic.dest_bin "op =" HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
 
-end);
+);
 *}
 
 ML {*
diff -r f339dc43ce9f -r 7eef2b183032 src/Provers/Arith/abel_cancel.ML
--- a/src/Provers/Arith/abel_cancel.ML	Wed Jun 18 16:55:44 2008 +0200
+++ b/src/Provers/Arith/abel_cancel.ML	Wed Jun 18 18:54:57 2008 +0200
@@ -12,10 +12,10 @@
 
 signature ABEL_CANCEL =
 sig
+  val eq_reflection   : thm           (*object-equality to meta-equality*)
+  val T               : typ           (*the type of group elements*)
   val cancel_ss       : simpset       (*abelian group cancel simpset*)
-  val thy_ref         : theory_ref    (*signature of the theory of the group*)
-  val T               : typ           (*the type of group elements*)
-  val eq_reflection   : thm           (*object-equality to meta-equality*)
+  val sum_pats        : cterm list
   val eqI_rules       : thm list
   val dest_eqI        : thm -> term
 end;
@@ -89,9 +89,7 @@
 
 val sum_conv =
   Simplifier.mk_simproc "cancel_sums"
-    (map (Drule.cterm_fun Logic.varify o Thm.read_cterm (Theory.deref thy_ref))
-      [("x + y", Data.T), ("x - y", Data.T)])  (* FIXME depends on concrete syntax *)
-    (K sum_proc);
+    (map (Drule.cterm_fun Logic.varify) Data.sum_pats) (K sum_proc);
 
 
 (*A simproc to cancel like terms on the opposite sides of relations:
@@ -109,6 +107,6 @@
 
 val rel_conv =
   Simplifier.mk_simproc "cancel_relations"
-    (map (Thm.cterm_of (Theory.deref thy_ref) o Data.dest_eqI) eqI_rules) (K rel_proc);
+    (map (fn th => Thm.cterm_of (Thm.theory_of_thm th) (Data.dest_eqI th)) eqI_rules) (K rel_proc);
 
 end;