--- 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 =
--- 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*)
--- 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 =
--- 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*)
--- 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;
--- 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;
--- 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. *)
(* *)
--- 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. *)
(* *)
--- 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 ->
--- 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) *)
--- 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 **)
--- 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
--- 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*)