got rid of type Sign.sg;
authorwenzelm
Sat Mar 11 21:23:10 2006 +0100 (2006-03-11 ago)
changeset 19250932a50e2332f
parent 19249 86c73395c99b
child 19251 6bc0dda66f32
got rid of type Sign.sg;
src/HOL/Integ/cooper_proof.ML
src/HOL/Integ/qelim.ML
src/HOL/Tools/Presburger/cooper_proof.ML
src/HOL/Tools/Presburger/qelim.ML
src/HOL/Tools/datatype_aux.ML
src/Provers/Arith/cancel_factor.ML
src/Provers/order.ML
src/Provers/quasi.ML
src/Pure/IsaPlanner/isa_fterm.ML
src/Pure/IsaPlanner/isand.ML
src/Pure/sign.ML
src/Pure/type.ML
src/ZF/arith_data.ML
     1.1 --- a/src/HOL/Integ/cooper_proof.ML	Sat Mar 11 17:30:35 2006 +0100
     1.2 +++ b/src/HOL/Integ/cooper_proof.ML	Sat Mar 11 21:23:10 2006 +0100
     1.3 @@ -17,13 +17,13 @@
     1.4    val qe_exI : thm
     1.5    val list_to_set : typ -> term list -> term
     1.6    val qe_get_terms : thm -> term * term
     1.7 -  val cooper_prv  : Sign.sg -> term -> term -> thm
     1.8 -  val proof_of_evalc : Sign.sg -> term -> thm
     1.9 -  val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm
    1.10 -  val proof_of_linform : Sign.sg -> string list -> term -> thm
    1.11 -  val proof_of_adjustcoeffeq : Sign.sg -> term -> IntInf.int -> term -> thm
    1.12 -  val prove_elementar : Sign.sg -> string -> term -> thm
    1.13 -  val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
    1.14 +  val cooper_prv  : theory -> term -> term -> thm
    1.15 +  val proof_of_evalc : theory -> term -> thm
    1.16 +  val proof_of_cnnf : theory -> term -> (term -> thm) -> thm
    1.17 +  val proof_of_linform : theory -> string list -> term -> thm
    1.18 +  val proof_of_adjustcoeffeq : theory -> term -> IntInf.int -> term -> thm
    1.19 +  val prove_elementar : theory -> string -> term -> thm
    1.20 +  val thm_of : theory -> (term -> (term list * (thm list -> thm))) -> term -> thm
    1.21  end;
    1.22  
    1.23  structure CooperProof : COOPER_PROOF =
     2.1 --- a/src/HOL/Integ/qelim.ML	Sat Mar 11 17:30:35 2006 +0100
     2.2 +++ b/src/HOL/Integ/qelim.ML	Sat Mar 11 21:23:10 2006 +0100
     2.3 @@ -8,7 +8,7 @@
     2.4  
     2.5  signature QELIM =
     2.6   sig
     2.7 - val tproof_of_mlift_qelim: Sign.sg -> (term -> bool) ->
     2.8 + val tproof_of_mlift_qelim: theory -> (term -> bool) ->
     2.9     (string list -> term -> thm) -> (term -> thm) ->
    2.10     (term -> thm) -> term -> thm
    2.11  
    2.12 @@ -19,7 +19,7 @@
    2.13  open CooperDec;
    2.14  open CooperProof;
    2.15  
    2.16 -val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
    2.17 +val cboolT = ctyp_of HOL.thy HOLogic.boolT;
    2.18  
    2.19  (* List of the theorems to be used in the following*)
    2.20  
     3.1 --- a/src/HOL/Tools/Presburger/cooper_proof.ML	Sat Mar 11 17:30:35 2006 +0100
     3.2 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Sat Mar 11 21:23:10 2006 +0100
     3.3 @@ -17,13 +17,13 @@
     3.4    val qe_exI : thm
     3.5    val list_to_set : typ -> term list -> term
     3.6    val qe_get_terms : thm -> term * term
     3.7 -  val cooper_prv  : Sign.sg -> term -> term -> thm
     3.8 -  val proof_of_evalc : Sign.sg -> term -> thm
     3.9 -  val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm
    3.10 -  val proof_of_linform : Sign.sg -> string list -> term -> thm
    3.11 -  val proof_of_adjustcoeffeq : Sign.sg -> term -> IntInf.int -> term -> thm
    3.12 -  val prove_elementar : Sign.sg -> string -> term -> thm
    3.13 -  val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
    3.14 +  val cooper_prv  : theory -> term -> term -> thm
    3.15 +  val proof_of_evalc : theory -> term -> thm
    3.16 +  val proof_of_cnnf : theory -> term -> (term -> thm) -> thm
    3.17 +  val proof_of_linform : theory -> string list -> term -> thm
    3.18 +  val proof_of_adjustcoeffeq : theory -> term -> IntInf.int -> term -> thm
    3.19 +  val prove_elementar : theory -> string -> term -> thm
    3.20 +  val thm_of : theory -> (term -> (term list * (thm list -> thm))) -> term -> thm
    3.21  end;
    3.22  
    3.23  structure CooperProof : COOPER_PROOF =
     4.1 --- a/src/HOL/Tools/Presburger/qelim.ML	Sat Mar 11 17:30:35 2006 +0100
     4.2 +++ b/src/HOL/Tools/Presburger/qelim.ML	Sat Mar 11 21:23:10 2006 +0100
     4.3 @@ -8,7 +8,7 @@
     4.4  
     4.5  signature QELIM =
     4.6   sig
     4.7 - val tproof_of_mlift_qelim: Sign.sg -> (term -> bool) ->
     4.8 + val tproof_of_mlift_qelim: theory -> (term -> bool) ->
     4.9     (string list -> term -> thm) -> (term -> thm) ->
    4.10     (term -> thm) -> term -> thm
    4.11  
    4.12 @@ -19,7 +19,7 @@
    4.13  open CooperDec;
    4.14  open CooperProof;
    4.15  
    4.16 -val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
    4.17 +val cboolT = ctyp_of HOL.thy HOLogic.boolT;
    4.18  
    4.19  (* List of the theorems to be used in the following*)
    4.20  
     5.1 --- a/src/HOL/Tools/datatype_aux.ML	Sat Mar 11 17:30:35 2006 +0100
     5.2 +++ b/src/HOL/Tools/datatype_aux.ML	Sat Mar 11 21:23:10 2006 +0100
     5.3 @@ -62,7 +62,7 @@
     5.4    val get_rec_types : descr -> (string * sort) list -> typ list
     5.5    val check_nonempty : descr list -> unit
     5.6    val unfold_datatypes : 
     5.7 -    Sign.sg -> descr -> (string * sort) list -> datatype_info Symtab.table ->
     5.8 +    theory -> descr -> (string * sort) list -> datatype_info Symtab.table ->
     5.9        descr -> int -> descr list * int
    5.10  end;
    5.11  
     6.1 --- a/src/Provers/Arith/cancel_factor.ML	Sat Mar 11 17:30:35 2006 +0100
     6.2 +++ b/src/Provers/Arith/cancel_factor.ML	Sat Mar 11 21:23:10 2006 +0100
     6.3 @@ -13,14 +13,14 @@
     6.4    val mk_bal: term * term -> term
     6.5    val dest_bal: term -> term * term
     6.6    (*rules*)
     6.7 -  val prove_conv: tactic -> tactic -> Sign.sg -> term * term -> thm
     6.8 +  val prove_conv: tactic -> tactic -> theory -> term * term -> thm
     6.9    val norm_tac: tactic			(*AC0 etc.*)
    6.10    val multiply_tac: IntInf.int -> tactic	(*apply a ~~ b  ==  k * a ~~ k * b  (for k > 0)*)
    6.11  end;
    6.12  
    6.13  signature CANCEL_FACTOR =
    6.14  sig
    6.15 -  val proc: Sign.sg -> thm list -> term -> thm option
    6.16 +  val proc: theory -> thm list -> term -> thm option
    6.17  end;
    6.18  
    6.19  
     7.1 --- a/src/Provers/order.ML	Sat Mar 11 17:30:35 2006 +0100
     7.2 +++ b/src/Provers/order.ML	Sat Mar 11 21:23:10 2006 +0100
     7.3 @@ -61,9 +61,9 @@
     7.4         where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=",
     7.5         other relation symbols cause an error message *)
     7.6    (* decomp_part is used by partial_tac *)
     7.7 -  val decomp_part: Sign.sg -> term -> (term * string * term) option
     7.8 +  val decomp_part: theory -> term -> (term * string * term) option
     7.9    (* decomp_lin is used by linear_tac *)
    7.10 -  val decomp_lin: Sign.sg -> term -> (term * string * term) option
    7.11 +  val decomp_lin: theory -> term -> (term * string * term) option
    7.12  end;
    7.13  
    7.14  signature ORDER_TAC  =
    7.15 @@ -117,7 +117,7 @@
    7.16  
    7.17  (* ************************************************************************ *)
    7.18  (*                                                                          *)
    7.19 -(* mkasm_partial sign (t, n) : Sign.sg -> (Term.term * int) -> less         *)
    7.20 +(* mkasm_partial sign (t, n) : theory -> (Term.term * int) -> less          *)
    7.21  (*                                                                          *)
    7.22  (* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
    7.23  (* translated to an element of type less.                                   *)
    7.24 @@ -145,7 +145,7 @@
    7.25  
    7.26  (* ************************************************************************ *)
    7.27  (*                                                                          *)
    7.28 -(* mkasm_linear sign (t, n) : Sign.sg -> (Term.term * int) -> less          *)
    7.29 +(* mkasm_linear sign (t, n) : theory -> (Term.term * int) -> less           *)
    7.30  (*                                                                          *)
    7.31  (* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
    7.32  (* translated to an element of type less.                                   *)
    7.33 @@ -175,7 +175,7 @@
    7.34  
    7.35  (* ************************************************************************ *)
    7.36  (*                                                                          *)
    7.37 -(* mkconcl_partial sign t : Sign.sg -> Term.term -> less                    *)
    7.38 +(* mkconcl_partial sign t : theory -> Term.term -> less                     *)
    7.39  (*                                                                          *)
    7.40  (* Translates conclusion t to an element of type less.                      *)
    7.41  (* Partial orders only.                                                     *)
    7.42 @@ -195,7 +195,7 @@
    7.43  
    7.44  (* ************************************************************************ *)
    7.45  (*                                                                          *)
    7.46 -(* mkconcl_linear sign t : Sign.sg -> Term.term -> less                     *)
    7.47 +(* mkconcl_linear sign t : theory -> Term.term -> less                      *)
    7.48  (*                                                                          *)
    7.49  (* Translates conclusion t to an element of type less.                      *)
    7.50  (* Linear orders only.                                                      *)
    7.51 @@ -1010,7 +1010,7 @@
    7.52  (* *********************************************************************** *)
    7.53  (*                                                                         *)
    7.54  (* solvePartialOrder sign (asms,concl) :                                   *)
    7.55 -(* Sign.sg -> less list * Term.term -> proof list                          *)
    7.56 +(* theory -> less list * Term.term -> proof list                           *)
    7.57  (*                                                                         *)
    7.58  (* Find proof if possible for partial orders.                              *)
    7.59  (*                                                                         *)
    7.60 @@ -1036,7 +1036,7 @@
    7.61  (* *********************************************************************** *)
    7.62  (*                                                                         *)
    7.63  (* solveTotalOrder sign (asms,concl) :                                     *)
    7.64 -(* Sign.sg -> less list * Term.term -> proof list                          *)
    7.65 +(* theory -> less list * Term.term -> proof list                           *)
    7.66  (*                                                                         *)
    7.67  (* Find proof if possible for linear orders.                               *)
    7.68  (*                                                                         *)
     8.1 --- a/src/Provers/quasi.ML	Sat Mar 11 17:30:35 2006 +0100
     8.2 +++ b/src/Provers/quasi.ML	Sat Mar 11 21:23:10 2006 +0100
     8.3 @@ -61,9 +61,9 @@
     8.4         where Rel is one of "<", "<=", "=" and "~=",
     8.5         other relation symbols cause an error message *)
     8.6    (* decomp_trans is used by trans_tac, it may only return Rel = "<=" *)
     8.7 -  val decomp_trans: Sign.sg -> term -> (term * string * term) option
     8.8 +  val decomp_trans: theory -> term -> (term * string * term) option
     8.9    (* decomp_quasi is used by quasi_tac *)
    8.10 -  val decomp_quasi: Sign.sg -> term -> (term * string * term) option
    8.11 +  val decomp_quasi: theory -> term -> (term * string * term) option
    8.12  end;
    8.13  
    8.14  signature QUASI_TAC = 
    8.15 @@ -117,7 +117,7 @@
    8.16  
    8.17  (* ************************************************************************ *)
    8.18  (*                                                                          *)
    8.19 -(* mkasm_trans sign (t, n) :  Sign.sg -> (Term.term * int)  -> less         *)
    8.20 +(* mkasm_trans sign (t, n) :  theory -> (Term.term * int)  -> less          *)
    8.21  (*                                                                          *)
    8.22  (* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
    8.23  (* translated to an element of type less.                                   *)
    8.24 @@ -136,7 +136,7 @@
    8.25    
    8.26  (* ************************************************************************ *)
    8.27  (*                                                                          *)
    8.28 -(* mkasm_quasi sign (t, n) : Sign.sg -> (Term.term * int) -> less           *)
    8.29 +(* mkasm_quasi sign (t, n) : theory -> (Term.term * int) -> less            *)
    8.30  (*                                                                          *)
    8.31  (* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
    8.32  (* translated to an element of type less.                                   *)
    8.33 @@ -163,7 +163,7 @@
    8.34  
    8.35  (* ************************************************************************ *)
    8.36  (*                                                                          *)
    8.37 -(* mkconcl_trans sign t : Sign.sg -> Term.term -> less                      *)
    8.38 +(* mkconcl_trans sign t : theory -> Term.term -> less                       *)
    8.39  (*                                                                          *)
    8.40  (* Translates conclusion t to an element of type less.                      *)
    8.41  (* Only for Conclusions of form x <= y or x < y.                            *)
    8.42 @@ -181,7 +181,7 @@
    8.43    
    8.44  (* ************************************************************************ *)
    8.45  (*                                                                          *)
    8.46 -(* mkconcl_quasi sign t : Sign.sg -> Term.term -> less                      *)
    8.47 +(* mkconcl_quasi sign t : theory -> Term.term -> less                       *)
    8.48  (*                                                                          *)
    8.49  (* Translates conclusion t to an element of type less.                      *)
    8.50  (* Quasi orders only.                                                       *)
    8.51 @@ -504,7 +504,7 @@
    8.52  (* *********************************************************************** *)
    8.53  (*                                                                         *)
    8.54  (* solveLeTrans sign (asms,concl) :                                        *)
    8.55 -(* Sign.sg -> less list * Term.term -> proof list                          *)
    8.56 +(* theory -> less list * Term.term -> proof list                           *)
    8.57  (*                                                                         *)
    8.58  (* Solves                                                                  *)
    8.59  (*                                                                         *)
    8.60 @@ -527,7 +527,7 @@
    8.61  (* *********************************************************************** *)
    8.62  (*                                                                         *)
    8.63  (* solveQuasiOrder sign (asms,concl) :                                     *)
    8.64 -(* Sign.sg -> less list * Term.term -> proof list                          *)
    8.65 +(* theory -> less list * Term.term -> proof list                           *)
    8.66  (*                                                                         *)
    8.67  (* Find proof if possible for quasi order.                                 *)
    8.68  (*                                                                         *)
     9.1 --- a/src/Pure/IsaPlanner/isa_fterm.ML	Sat Mar 11 17:30:35 2006 +0100
     9.2 +++ b/src/Pure/IsaPlanner/isa_fterm.ML	Sat Mar 11 21:23:10 2006 +0100
     9.3 @@ -50,7 +50,7 @@
     9.4         * Term.term)
     9.5         option
     9.6      val clean_unify_ft :
     9.7 -       Sign.sg ->
     9.8 +       theory ->
     9.9         int ->
    9.10         Term.term ->
    9.11         FcTerm ->
    10.1 --- a/src/Pure/IsaPlanner/isand.ML	Sat Mar 11 17:30:35 2006 +0100
    10.2 +++ b/src/Pure/IsaPlanner/isand.ML	Sat Mar 11 21:23:10 2006 +0100
    10.3 @@ -56,7 +56,7 @@
    10.4    val allify_conditions' :
    10.5        (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
    10.6    val assume_allified :
    10.7 -      Sign.sg -> (string * Term.sort) list * (string * Term.typ) list
    10.8 +      theory -> (string * Term.sort) list * (string * Term.typ) list
    10.9        -> Term.term -> (Thm.cterm * Thm.thm)
   10.10  
   10.11    (* meta level fixed params (i.e. !! vars) *)
    11.1 --- a/src/Pure/sign.ML	Sat Mar 11 17:30:35 2006 +0100
    11.2 +++ b/src/Pure/sign.ML	Sat Mar 11 21:23:10 2006 +0100
    11.3 @@ -82,7 +82,6 @@
    11.4  
    11.5  signature SIGN =
    11.6  sig
    11.7 -  type sg    (*obsolete*)
    11.8    val init_data: theory -> theory
    11.9    val rep_sg: theory ->
   11.10     {naming: NameSpace.naming,
   11.11 @@ -200,8 +199,6 @@
   11.12  structure Sign: SIGN =
   11.13  struct
   11.14  
   11.15 -type sg = theory;
   11.16 -
   11.17  
   11.18  (** datatype sign **)
   11.19  
    12.1 --- a/src/Pure/type.ML	Sat Mar 11 17:30:35 2006 +0100
    12.2 +++ b/src/Pure/type.ML	Sat Mar 11 21:23:10 2006 +0100
    12.3 @@ -480,7 +480,7 @@
    12.4    | SOME Ss' =>
    12.5        if Sorts.sorts_le C (Ss, Ss') then ars
    12.6        else if Sorts.sorts_le C (Ss', Ss)
    12.7 -      then coregular pp C t (c, Ss) (ars \ (c, Ss'))
    12.8 +      then coregular pp C t (c, Ss) (remove (op =) (c, Ss') ars)
    12.9        else err_conflict pp t NONE (c, Ss) (c, Ss'));
   12.10  
   12.11  fun complete C (c, Ss) = map (rpair Ss) (Graph.all_succs C [c]);
   12.12 @@ -619,8 +619,7 @@
   12.13  
   12.14  fun add_abbrev naming (a, vs, rhs) tsig = tsig |> change_types (fn types =>
   12.15    let
   12.16 -    fun err msg =
   12.17 -      error (msg ^ "\nThe error(s) above occurred in type abbreviation: " ^ quote a);
   12.18 +    fun err msg = cat_error msg ("The error(s) above occurred in type abbreviation: " ^ quote a);
   12.19      val rhs' = strip_sorts (no_tvars (cert_typ_syntax tsig rhs))
   12.20        handle TYPE (msg, _, _) => err msg;
   12.21    in
    13.1 --- a/src/ZF/arith_data.ML	Sat Mar 11 17:30:35 2006 +0100
    13.2 +++ b/src/ZF/arith_data.ML	Sat Mar 11 21:23:10 2006 +0100
    13.3 @@ -12,7 +12,7 @@
    13.4    val nat_cancel: simproc list
    13.5    (*tools for use in similar applications*)
    13.6    val gen_trans_tac: thm -> thm option -> tactic
    13.7 -  val prove_conv: string -> tactic list -> Sign.sg ->
    13.8 +  val prove_conv: string -> tactic list -> theory ->
    13.9                    thm list -> string list -> term * term -> thm option
   13.10    val simplify_meta_eq: thm list -> simpset -> thm -> thm
   13.11    (*debugging*)