# HG changeset patch
# User wenzelm
# Date 1119025983 -7200
# Node ID 24abe4c0e4b498e581ea25606a69c9975726d094
# Parent  9aa6d9cf2832da501c5bfa50bf0394ca25591a46
renamed sg_ref to thy_ref;

diff -r 9aa6d9cf2832 -r 24abe4c0e4b4 src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Fri Jun 17 18:33:03 2005 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Fri Jun 17 18:33:03 2005 +0200
@@ -466,7 +466,7 @@
 struct
   val ss                = HOL_ss
   val eq_reflection     = eq_reflection
-  val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
+  val thy_ref = Theory.self_ref (the_context ())
   val add_ac = mult_ac
 end;
 
diff -r 9aa6d9cf2832 -r 24abe4c0e4b4 src/HOL/OrderedGroup.ML
--- a/src/HOL/OrderedGroup.ML	Fri Jun 17 18:33:03 2005 +0200
+++ b/src/HOL/OrderedGroup.ML	Fri Jun 17 18:33:03 2005 +0200
@@ -8,7 +8,7 @@
   val ss = simpset_of HOL.thy
   val eq_reflection = thm "eq_reflection"
   
-  val sg_ref = Sign.self_ref (sign_of (theory "OrderedGroup"))
+  val thy_ref = Theory.self_ref (theory "OrderedGroup")
 
   val T = TFree("'a", ["OrderedGroup.ab_group_add"])
   
diff -r 9aa6d9cf2832 -r 24abe4c0e4b4 src/Provers/Arith/abel_cancel.ML
--- a/src/Provers/Arith/abel_cancel.ML	Fri Jun 17 18:33:03 2005 +0200
+++ b/src/Provers/Arith/abel_cancel.ML	Fri Jun 17 18:33:03 2005 +0200
@@ -10,14 +10,14 @@
 
 *)
 
-(* Modificaton in May 2004 by Steven Obua: polymorphic types work also now *) 
+(* Modification in May 2004 by Steven Obua: polymorphic types work also now *) 
 
 signature ABEL_CANCEL =
 sig
   val ss                : simpset       (*basic simpset of object-logic*)
   val eq_reflection     : thm           (*object-equality to meta-equality*)
 
-  val sg_ref            : Sign.sg_ref   (*signature of the theory of the group*)
+  val thy_ref           : theory_ref    (*signature of the theory of the group*)
   val T                 : typ           (*the type of group elements*)
 
   val restrict_to_left  : thm
@@ -125,7 +125,7 @@
 
  val sum_conv =
      Simplifier.mk_simproc "cancel_sums"
-       (map (Drule.cterm_fun Logic.varify o Thm.read_cterm (Sign.deref sg_ref))
+       (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 !???!!??! *)
        sum_proc;
 
@@ -182,7 +182,7 @@
    handle Cancel => NONE;
 
  val rel_conv =
-     Simplifier.simproc_i (Sign.deref sg_ref) "cancel_relations"
+     Simplifier.simproc_i (Theory.deref thy_ref) "cancel_relations"
        (map Data.dest_eqI eqI_rules) rel_proc;
 
 end;
diff -r 9aa6d9cf2832 -r 24abe4c0e4b4 src/Provers/Arith/assoc_fold.ML
--- a/src/Provers/Arith/assoc_fold.ML	Fri Jun 17 18:33:03 2005 +0200
+++ b/src/Provers/Arith/assoc_fold.ML	Fri Jun 17 18:33:03 2005 +0200
@@ -13,7 +13,7 @@
 sig
   val ss                : simpset       (*basic simpset of object-logtic*)
   val eq_reflection     : thm           (*object-equality to meta-equality*)
-  val sg_ref            : Sign.sg_ref   (*the operator's signature*)
+  val thy_ref           : theory_ref    (*the operator's signature*)
   val add_ac            : thm list      (*AC-rewrites for plus*)
 end;
 
@@ -42,8 +42,8 @@
  val trace = ref false;
 
  (*Make a simproc to combine all literals in a associative nest*)
- fun proc sg _ lhs =
-   let fun show t = string_of_cterm (Thm.cterm_of sg t)
+ fun proc thy _ lhs =
+   let fun show t = string_of_cterm (Thm.cterm_of thy t)
        val _ = if !trace then tracing ("assoc_fold simproc: LHS = " ^ show lhs)
                else ()
        val plus =
@@ -54,7 +54,7 @@
                else ()
        val rhs = plus $ mk_sum plus lits $ mk_sum plus others
        val _ = if !trace then tracing ("RHS = " ^ show rhs) else ()
-       val th = Tactic.prove sg [] [] (Logic.mk_equals (lhs, rhs))
+       val th = Tactic.prove thy [] [] (Logic.mk_equals (lhs, rhs))
                    (fn _ => rtac Data.eq_reflection 1 THEN
                             simp_tac assoc_ss 1)
    in SOME th end