# HG changeset patch # User wenzelm # Date 1142108590 -3600 # Node ID 932a50e2332f5778b2926b44620fe38540398bea # Parent 86c73395c99bf368db2ab60e9661a633c7e4a309 got rid of type Sign.sg; diff -r 86c73395c99b -r 932a50e2332f src/HOL/Integ/cooper_proof.ML --- a/src/HOL/Integ/cooper_proof.ML Sat Mar 11 17:30:35 2006 +0100 +++ b/src/HOL/Integ/cooper_proof.ML Sat Mar 11 21:23:10 2006 +0100 @@ -17,13 +17,13 @@ val qe_exI : thm val list_to_set : typ -> term list -> term val qe_get_terms : thm -> term * term - val cooper_prv : Sign.sg -> term -> term -> thm - val proof_of_evalc : Sign.sg -> term -> thm - val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm - val proof_of_linform : Sign.sg -> string list -> term -> thm - val proof_of_adjustcoeffeq : Sign.sg -> term -> IntInf.int -> term -> thm - val prove_elementar : Sign.sg -> string -> term -> thm - val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm + val cooper_prv : theory -> term -> term -> thm + val proof_of_evalc : theory -> term -> thm + val proof_of_cnnf : theory -> term -> (term -> thm) -> thm + val proof_of_linform : theory -> string list -> term -> thm + val proof_of_adjustcoeffeq : theory -> term -> IntInf.int -> term -> thm + val prove_elementar : theory -> string -> term -> thm + val thm_of : theory -> (term -> (term list * (thm list -> thm))) -> term -> thm end; structure CooperProof : COOPER_PROOF = diff -r 86c73395c99b -r 932a50e2332f src/HOL/Integ/qelim.ML --- a/src/HOL/Integ/qelim.ML Sat Mar 11 17:30:35 2006 +0100 +++ b/src/HOL/Integ/qelim.ML Sat Mar 11 21:23:10 2006 +0100 @@ -8,7 +8,7 @@ signature QELIM = sig - val tproof_of_mlift_qelim: Sign.sg -> (term -> bool) -> + val tproof_of_mlift_qelim: theory -> (term -> bool) -> (string list -> term -> thm) -> (term -> thm) -> (term -> thm) -> term -> thm @@ -19,7 +19,7 @@ open CooperDec; open CooperProof; -val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT; +val cboolT = ctyp_of HOL.thy HOLogic.boolT; (* List of the theorems to be used in the following*) diff -r 86c73395c99b -r 932a50e2332f src/HOL/Tools/Presburger/cooper_proof.ML --- a/src/HOL/Tools/Presburger/cooper_proof.ML Sat Mar 11 17:30:35 2006 +0100 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML Sat Mar 11 21:23:10 2006 +0100 @@ -17,13 +17,13 @@ val qe_exI : thm val list_to_set : typ -> term list -> term val qe_get_terms : thm -> term * term - val cooper_prv : Sign.sg -> term -> term -> thm - val proof_of_evalc : Sign.sg -> term -> thm - val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm - val proof_of_linform : Sign.sg -> string list -> term -> thm - val proof_of_adjustcoeffeq : Sign.sg -> term -> IntInf.int -> term -> thm - val prove_elementar : Sign.sg -> string -> term -> thm - val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm + val cooper_prv : theory -> term -> term -> thm + val proof_of_evalc : theory -> term -> thm + val proof_of_cnnf : theory -> term -> (term -> thm) -> thm + val proof_of_linform : theory -> string list -> term -> thm + val proof_of_adjustcoeffeq : theory -> term -> IntInf.int -> term -> thm + val prove_elementar : theory -> string -> term -> thm + val thm_of : theory -> (term -> (term list * (thm list -> thm))) -> term -> thm end; structure CooperProof : COOPER_PROOF = diff -r 86c73395c99b -r 932a50e2332f src/HOL/Tools/Presburger/qelim.ML --- a/src/HOL/Tools/Presburger/qelim.ML Sat Mar 11 17:30:35 2006 +0100 +++ b/src/HOL/Tools/Presburger/qelim.ML Sat Mar 11 21:23:10 2006 +0100 @@ -8,7 +8,7 @@ signature QELIM = sig - val tproof_of_mlift_qelim: Sign.sg -> (term -> bool) -> + val tproof_of_mlift_qelim: theory -> (term -> bool) -> (string list -> term -> thm) -> (term -> thm) -> (term -> thm) -> term -> thm @@ -19,7 +19,7 @@ open CooperDec; open CooperProof; -val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT; +val cboolT = ctyp_of HOL.thy HOLogic.boolT; (* List of the theorems to be used in the following*) diff -r 86c73395c99b -r 932a50e2332f src/HOL/Tools/datatype_aux.ML --- a/src/HOL/Tools/datatype_aux.ML Sat Mar 11 17:30:35 2006 +0100 +++ b/src/HOL/Tools/datatype_aux.ML Sat Mar 11 21:23:10 2006 +0100 @@ -62,7 +62,7 @@ val get_rec_types : descr -> (string * sort) list -> typ list val check_nonempty : descr list -> unit val unfold_datatypes : - Sign.sg -> descr -> (string * sort) list -> datatype_info Symtab.table -> + theory -> descr -> (string * sort) list -> datatype_info Symtab.table -> descr -> int -> descr list * int end; diff -r 86c73395c99b -r 932a50e2332f src/Provers/Arith/cancel_factor.ML --- a/src/Provers/Arith/cancel_factor.ML Sat Mar 11 17:30:35 2006 +0100 +++ b/src/Provers/Arith/cancel_factor.ML Sat Mar 11 21:23:10 2006 +0100 @@ -13,14 +13,14 @@ val mk_bal: term * term -> term val dest_bal: term -> term * term (*rules*) - val prove_conv: tactic -> tactic -> Sign.sg -> term * term -> thm + val prove_conv: tactic -> tactic -> theory -> term * term -> thm val norm_tac: tactic (*AC0 etc.*) val multiply_tac: IntInf.int -> tactic (*apply a ~~ b == k * a ~~ k * b (for k > 0)*) end; signature CANCEL_FACTOR = sig - val proc: Sign.sg -> thm list -> term -> thm option + val proc: theory -> thm list -> term -> thm option end; diff -r 86c73395c99b -r 932a50e2332f src/Provers/order.ML --- a/src/Provers/order.ML Sat Mar 11 17:30:35 2006 +0100 +++ b/src/Provers/order.ML Sat Mar 11 21:23:10 2006 +0100 @@ -61,9 +61,9 @@ where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=", other relation symbols cause an error message *) (* decomp_part is used by partial_tac *) - val decomp_part: Sign.sg -> term -> (term * string * term) option + val decomp_part: theory -> term -> (term * string * term) option (* decomp_lin is used by linear_tac *) - val decomp_lin: Sign.sg -> term -> (term * string * term) option + val decomp_lin: theory -> term -> (term * string * term) option end; signature ORDER_TAC = @@ -117,7 +117,7 @@ (* ************************************************************************ *) (* *) -(* mkasm_partial sign (t, n) : Sign.sg -> (Term.term * int) -> less *) +(* mkasm_partial sign (t, n) : theory -> (Term.term * int) -> less *) (* *) (* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) (* translated to an element of type less. *) @@ -145,7 +145,7 @@ (* ************************************************************************ *) (* *) -(* mkasm_linear sign (t, n) : Sign.sg -> (Term.term * int) -> less *) +(* mkasm_linear sign (t, n) : theory -> (Term.term * int) -> less *) (* *) (* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) (* translated to an element of type less. *) @@ -175,7 +175,7 @@ (* ************************************************************************ *) (* *) -(* mkconcl_partial sign t : Sign.sg -> Term.term -> less *) +(* mkconcl_partial sign t : theory -> Term.term -> less *) (* *) (* Translates conclusion t to an element of type less. *) (* Partial orders only. *) @@ -195,7 +195,7 @@ (* ************************************************************************ *) (* *) -(* mkconcl_linear sign t : Sign.sg -> Term.term -> less *) +(* mkconcl_linear sign t : theory -> Term.term -> less *) (* *) (* Translates conclusion t to an element of type less. *) (* Linear orders only. *) @@ -1010,7 +1010,7 @@ (* *********************************************************************** *) (* *) (* solvePartialOrder sign (asms,concl) : *) -(* Sign.sg -> less list * Term.term -> proof list *) +(* theory -> less list * Term.term -> proof list *) (* *) (* Find proof if possible for partial orders. *) (* *) @@ -1036,7 +1036,7 @@ (* *********************************************************************** *) (* *) (* solveTotalOrder sign (asms,concl) : *) -(* Sign.sg -> less list * Term.term -> proof list *) +(* theory -> less list * Term.term -> proof list *) (* *) (* Find proof if possible for linear orders. *) (* *) diff -r 86c73395c99b -r 932a50e2332f src/Provers/quasi.ML --- a/src/Provers/quasi.ML Sat Mar 11 17:30:35 2006 +0100 +++ b/src/Provers/quasi.ML Sat Mar 11 21:23:10 2006 +0100 @@ -61,9 +61,9 @@ where Rel is one of "<", "<=", "=" and "~=", other relation symbols cause an error message *) (* decomp_trans is used by trans_tac, it may only return Rel = "<=" *) - val decomp_trans: Sign.sg -> term -> (term * string * term) option + val decomp_trans: theory -> term -> (term * string * term) option (* decomp_quasi is used by quasi_tac *) - val decomp_quasi: Sign.sg -> term -> (term * string * term) option + val decomp_quasi: theory -> term -> (term * string * term) option end; signature QUASI_TAC = @@ -117,7 +117,7 @@ (* ************************************************************************ *) (* *) -(* mkasm_trans sign (t, n) : Sign.sg -> (Term.term * int) -> less *) +(* mkasm_trans sign (t, n) : theory -> (Term.term * int) -> less *) (* *) (* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) (* translated to an element of type less. *) @@ -136,7 +136,7 @@ (* ************************************************************************ *) (* *) -(* mkasm_quasi sign (t, n) : Sign.sg -> (Term.term * int) -> less *) +(* mkasm_quasi sign (t, n) : theory -> (Term.term * int) -> less *) (* *) (* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) (* translated to an element of type less. *) @@ -163,7 +163,7 @@ (* ************************************************************************ *) (* *) -(* mkconcl_trans sign t : Sign.sg -> Term.term -> less *) +(* mkconcl_trans sign t : theory -> Term.term -> less *) (* *) (* Translates conclusion t to an element of type less. *) (* Only for Conclusions of form x <= y or x < y. *) @@ -181,7 +181,7 @@ (* ************************************************************************ *) (* *) -(* mkconcl_quasi sign t : Sign.sg -> Term.term -> less *) +(* mkconcl_quasi sign t : theory -> Term.term -> less *) (* *) (* Translates conclusion t to an element of type less. *) (* Quasi orders only. *) @@ -504,7 +504,7 @@ (* *********************************************************************** *) (* *) (* solveLeTrans sign (asms,concl) : *) -(* Sign.sg -> less list * Term.term -> proof list *) +(* theory -> less list * Term.term -> proof list *) (* *) (* Solves *) (* *) @@ -527,7 +527,7 @@ (* *********************************************************************** *) (* *) (* solveQuasiOrder sign (asms,concl) : *) -(* Sign.sg -> less list * Term.term -> proof list *) +(* theory -> less list * Term.term -> proof list *) (* *) (* Find proof if possible for quasi order. *) (* *) diff -r 86c73395c99b -r 932a50e2332f src/Pure/IsaPlanner/isa_fterm.ML --- a/src/Pure/IsaPlanner/isa_fterm.ML Sat Mar 11 17:30:35 2006 +0100 +++ b/src/Pure/IsaPlanner/isa_fterm.ML Sat Mar 11 21:23:10 2006 +0100 @@ -50,7 +50,7 @@ * Term.term) option val clean_unify_ft : - Sign.sg -> + theory -> int -> Term.term -> FcTerm -> diff -r 86c73395c99b -r 932a50e2332f src/Pure/IsaPlanner/isand.ML --- a/src/Pure/IsaPlanner/isand.ML Sat Mar 11 17:30:35 2006 +0100 +++ b/src/Pure/IsaPlanner/isand.ML Sat Mar 11 21:23:10 2006 +0100 @@ -56,7 +56,7 @@ val allify_conditions' : (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list val assume_allified : - Sign.sg -> (string * Term.sort) list * (string * Term.typ) list + theory -> (string * Term.sort) list * (string * Term.typ) list -> Term.term -> (Thm.cterm * Thm.thm) (* meta level fixed params (i.e. !! vars) *) diff -r 86c73395c99b -r 932a50e2332f src/Pure/sign.ML --- a/src/Pure/sign.ML Sat Mar 11 17:30:35 2006 +0100 +++ b/src/Pure/sign.ML Sat Mar 11 21:23:10 2006 +0100 @@ -82,7 +82,6 @@ signature SIGN = sig - type sg (*obsolete*) val init_data: theory -> theory val rep_sg: theory -> {naming: NameSpace.naming, @@ -200,8 +199,6 @@ structure Sign: SIGN = struct -type sg = theory; - (** datatype sign **) diff -r 86c73395c99b -r 932a50e2332f src/Pure/type.ML --- a/src/Pure/type.ML Sat Mar 11 17:30:35 2006 +0100 +++ b/src/Pure/type.ML Sat Mar 11 21:23:10 2006 +0100 @@ -480,7 +480,7 @@ | SOME Ss' => if Sorts.sorts_le C (Ss, Ss') then ars else if Sorts.sorts_le C (Ss', Ss) - then coregular pp C t (c, Ss) (ars \ (c, Ss')) + then coregular pp C t (c, Ss) (remove (op =) (c, Ss') ars) else err_conflict pp t NONE (c, Ss) (c, Ss')); fun complete C (c, Ss) = map (rpair Ss) (Graph.all_succs C [c]); @@ -619,8 +619,7 @@ fun add_abbrev naming (a, vs, rhs) tsig = tsig |> change_types (fn types => let - fun err msg = - error (msg ^ "\nThe error(s) above occurred in type abbreviation: " ^ quote a); + fun err msg = cat_error msg ("The error(s) above occurred in type abbreviation: " ^ quote a); val rhs' = strip_sorts (no_tvars (cert_typ_syntax tsig rhs)) handle TYPE (msg, _, _) => err msg; in diff -r 86c73395c99b -r 932a50e2332f src/ZF/arith_data.ML --- a/src/ZF/arith_data.ML Sat Mar 11 17:30:35 2006 +0100 +++ b/src/ZF/arith_data.ML Sat Mar 11 21:23:10 2006 +0100 @@ -12,7 +12,7 @@ val nat_cancel: simproc list (*tools for use in similar applications*) val gen_trans_tac: thm -> thm option -> tactic - val prove_conv: string -> tactic list -> Sign.sg -> + val prove_conv: string -> tactic list -> theory -> thm list -> string list -> term * term -> thm option val simplify_meta_eq: thm list -> simpset -> thm -> thm (*debugging*)