renamed sg_ref to thy_ref;
authorwenzelm
Fri Jun 17 18:33:03 2005 +0200 (2005-06-17)
changeset 1642324abe4c0e4b4
parent 16422 9aa6d9cf2832
child 16424 18a07ad8fea8
renamed sg_ref to thy_ref;
src/HOL/Integ/int_arith1.ML
src/HOL/OrderedGroup.ML
src/Provers/Arith/abel_cancel.ML
src/Provers/Arith/assoc_fold.ML
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Fri Jun 17 18:33:03 2005 +0200
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Fri Jun 17 18:33:03 2005 +0200
     1.3 @@ -466,7 +466,7 @@
     1.4  struct
     1.5    val ss                = HOL_ss
     1.6    val eq_reflection     = eq_reflection
     1.7 -  val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
     1.8 +  val thy_ref = Theory.self_ref (the_context ())
     1.9    val add_ac = mult_ac
    1.10  end;
    1.11  
     2.1 --- a/src/HOL/OrderedGroup.ML	Fri Jun 17 18:33:03 2005 +0200
     2.2 +++ b/src/HOL/OrderedGroup.ML	Fri Jun 17 18:33:03 2005 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4    val ss = simpset_of HOL.thy
     2.5    val eq_reflection = thm "eq_reflection"
     2.6    
     2.7 -  val sg_ref = Sign.self_ref (sign_of (theory "OrderedGroup"))
     2.8 +  val thy_ref = Theory.self_ref (theory "OrderedGroup")
     2.9  
    2.10    val T = TFree("'a", ["OrderedGroup.ab_group_add"])
    2.11    
     3.1 --- a/src/Provers/Arith/abel_cancel.ML	Fri Jun 17 18:33:03 2005 +0200
     3.2 +++ b/src/Provers/Arith/abel_cancel.ML	Fri Jun 17 18:33:03 2005 +0200
     3.3 @@ -10,14 +10,14 @@
     3.4  
     3.5  *)
     3.6  
     3.7 -(* Modificaton in May 2004 by Steven Obua: polymorphic types work also now *) 
     3.8 +(* Modification in May 2004 by Steven Obua: polymorphic types work also now *) 
     3.9  
    3.10  signature ABEL_CANCEL =
    3.11  sig
    3.12    val ss                : simpset       (*basic simpset of object-logic*)
    3.13    val eq_reflection     : thm           (*object-equality to meta-equality*)
    3.14  
    3.15 -  val sg_ref            : Sign.sg_ref   (*signature of the theory of the group*)
    3.16 +  val thy_ref           : theory_ref    (*signature of the theory of the group*)
    3.17    val T                 : typ           (*the type of group elements*)
    3.18  
    3.19    val restrict_to_left  : thm
    3.20 @@ -125,7 +125,7 @@
    3.21  
    3.22   val sum_conv =
    3.23       Simplifier.mk_simproc "cancel_sums"
    3.24 -       (map (Drule.cterm_fun Logic.varify o Thm.read_cterm (Sign.deref sg_ref))
    3.25 +       (map (Drule.cterm_fun Logic.varify o Thm.read_cterm (Theory.deref thy_ref))
    3.26          [("x + y", Data.T), ("x - y", Data.T)])  (* FIXME depends on concrete syntax !???!!??! *)
    3.27         sum_proc;
    3.28  
    3.29 @@ -182,7 +182,7 @@
    3.30     handle Cancel => NONE;
    3.31  
    3.32   val rel_conv =
    3.33 -     Simplifier.simproc_i (Sign.deref sg_ref) "cancel_relations"
    3.34 +     Simplifier.simproc_i (Theory.deref thy_ref) "cancel_relations"
    3.35         (map Data.dest_eqI eqI_rules) rel_proc;
    3.36  
    3.37  end;
     4.1 --- a/src/Provers/Arith/assoc_fold.ML	Fri Jun 17 18:33:03 2005 +0200
     4.2 +++ b/src/Provers/Arith/assoc_fold.ML	Fri Jun 17 18:33:03 2005 +0200
     4.3 @@ -13,7 +13,7 @@
     4.4  sig
     4.5    val ss                : simpset       (*basic simpset of object-logtic*)
     4.6    val eq_reflection     : thm           (*object-equality to meta-equality*)
     4.7 -  val sg_ref            : Sign.sg_ref   (*the operator's signature*)
     4.8 +  val thy_ref           : theory_ref    (*the operator's signature*)
     4.9    val add_ac            : thm list      (*AC-rewrites for plus*)
    4.10  end;
    4.11  
    4.12 @@ -42,8 +42,8 @@
    4.13   val trace = ref false;
    4.14  
    4.15   (*Make a simproc to combine all literals in a associative nest*)
    4.16 - fun proc sg _ lhs =
    4.17 -   let fun show t = string_of_cterm (Thm.cterm_of sg t)
    4.18 + fun proc thy _ lhs =
    4.19 +   let fun show t = string_of_cterm (Thm.cterm_of thy t)
    4.20         val _ = if !trace then tracing ("assoc_fold simproc: LHS = " ^ show lhs)
    4.21                 else ()
    4.22         val plus =
    4.23 @@ -54,7 +54,7 @@
    4.24                 else ()
    4.25         val rhs = plus $ mk_sum plus lits $ mk_sum plus others
    4.26         val _ = if !trace then tracing ("RHS = " ^ show rhs) else ()
    4.27 -       val th = Tactic.prove sg [] [] (Logic.mk_equals (lhs, rhs))
    4.28 +       val th = Tactic.prove thy [] [] (Logic.mk_equals (lhs, rhs))
    4.29                     (fn _ => rtac Data.eq_reflection 1 THEN
    4.30                              simp_tac assoc_ss 1)
    4.31     in SOME th end