# HG changeset patch
# User paulson
# Date 907575561 -7200
# Node ID 377acd99d74cb6676bba49704395e6e4e6f1d9fa
# Parent  03d74c85a8183a5585c305c373e6fbe95405f961
simpler interface for Abel_Cancel

diff -r 03d74c85a818 -r 377acd99d74c src/HOL/Integ/simproc.ML
--- a/src/HOL/Integ/simproc.ML	Mon Oct 05 10:15:01 1998 +0200
+++ b/src/HOL/Integ/simproc.ML	Mon Oct 05 10:19:21 1998 +0200
@@ -28,8 +28,7 @@
 structure Int_Cancel_Data =
 struct
   val ss		= HOL_ss
-  val mk_eq		= HOLogic.mk_Trueprop o HOLogic.mk_eq
-  fun mk_meta_eq r	= r RS eq_reflection
+  val eq_reflection	= eq_reflection
 
   val thy	= IntDef.thy
   val T		= Type ("IntDef.int", [])
diff -r 03d74c85a818 -r 377acd99d74c src/HOL/Real/simproc.ML
--- a/src/HOL/Real/simproc.ML	Mon Oct 05 10:15:01 1998 +0200
+++ b/src/HOL/Real/simproc.ML	Mon Oct 05 10:19:21 1998 +0200
@@ -27,8 +27,7 @@
 structure Real_Cancel_Data =
 struct
   val ss		= HOL_ss
-  val mk_eq		= HOLogic.mk_Trueprop o HOLogic.mk_eq
-  fun mk_meta_eq r	= r RS eq_reflection
+  val eq_reflection	= eq_reflection
 
   val thy		= RealDef.thy
   val T			= Type ("RealDef.real", [])
diff -r 03d74c85a818 -r 377acd99d74c src/Provers/Arith/abel_cancel.ML
--- a/src/Provers/Arith/abel_cancel.ML	Mon Oct 05 10:15:01 1998 +0200
+++ b/src/Provers/Arith/abel_cancel.ML	Mon Oct 05 10:19:21 1998 +0200
@@ -12,22 +12,21 @@
 
 signature ABEL_CANCEL =
 sig
-  val ss	: simpset		(*basic simpset of object-logtic*)
-  val mk_eq     : term * term -> term	(*create an equality proposition*)
-  val mk_meta_eq: thm -> thm		(*object-equality to meta-equality*)
+  val ss		: simpset	(*basic simpset of object-logtic*)
+  val eq_reflection	: thm		(*object-equality to meta-equality*)
 
-  val thy	: theory		(*the theory of the group*)
-  val T		: typ			(*the type of group elements*)
+  val thy		: theory	(*the theory of the group*)
+  val T			: typ		(*the type of group elements*)
 
-  val zero	: term
+  val zero		: term
   val add_cancel_21	: thm
   val add_cancel_end	: thm
   val add_left_cancel	: thm
-  val add_assoc	: thm
-  val add_commute : thm
-  val add_left_commute : thm
-  val add_0 : thm
-  val add_0_right : thm
+  val add_assoc		: thm
+  val add_commute 	: thm
+  val add_left_commute 	: thm
+  val add_0 		: thm
+  val add_0_right 	: thm
 
   val eq_diff_eq 	: thm
   val eqI_rules		: thm list
@@ -113,15 +112,16 @@
        val _ = if !trace then 
 		 writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
 	       else ()
-       val ct = Thm.cterm_of sg (Data.mk_eq (lhs, rhs))
+       val ct = Thm.cterm_of sg (Logic.mk_equals (lhs, rhs))
        val thm = prove ct 
-		   (fn _ => [simp_tac prepare_ss 1,
+		   (fn _ => [rtac eq_reflection 1,
+			     simp_tac prepare_ss 1,
 			     IF_UNSOLVED (simp_tac cancel_ss 1),
 			     IF_UNSOLVED (simp_tac inverse_ss 1)])
 	 handle ERROR =>
 	 error("cancel_sums simproc:\nfailed to prove " ^
 	       string_of_cterm ct)
-   in Some (Data.mk_meta_eq thm) end
+   in Some thm end
    handle Cancel => None;
 
 
@@ -170,17 +170,18 @@
        val _ = if !trace then 
 		 writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
 	       else ()
-       val ct = Thm.cterm_of sg (Data.mk_eq (lhs,rhs))
+       val ct = Thm.cterm_of sg (Logic.mk_equals (lhs,rhs))
 
        val thm = prove ct 
-		   (fn _ => [resolve_tac eqI_rules 1,
+		   (fn _ => [rtac eq_reflection 1,
+			     resolve_tac eqI_rules 1,
 			     simp_tac prepare_ss 1,
 			     simp_tac sum_cancel_ss 1,
 			     IF_UNSOLVED (simp_tac add_ac_ss 1)])
 	 handle ERROR =>
 	 error("cancel_relations simproc:\nfailed to prove " ^
 	       string_of_cterm ct)
-   in Some (Data.mk_meta_eq thm) end
+   in Some thm end
    handle Cancel => None;
 
  val rel_conv =