--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Tue Oct 27 17:34:00 2009 +0100
@@ -28,8 +28,8 @@
val goal_thm_of : Proof.state -> thm
val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
Proof.state -> bool
- val theorems_in_proof_term : Thm.thm -> Thm.thm list
- val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list
+ val theorems_in_proof_term : thm -> thm list
+ val theorems_of_sucessful_proof : Toplevel.state option -> thm list
val get_setting : (string * string) list -> string * string -> string
val get_int_setting : (string * string) list -> string * int -> int
val cpu_time : ('a -> 'b) -> 'a -> 'b * int
--- a/src/HOL/SMT/Tools/smt_normalize.ML Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_normalize.ML Tue Oct 27 17:34:00 2009 +0100
@@ -14,8 +14,8 @@
signature SMT_NORMALIZE =
sig
val normalize_rule: Proof.context -> thm -> thm
- val instantiate_free: Thm.cterm * Thm.cterm -> thm -> thm
- val discharge_definition: Thm.cterm -> thm -> thm
+ val instantiate_free: cterm * cterm -> thm -> thm
+ val discharge_definition: cterm -> thm -> thm
val trivial_let: Proof.context -> thm list -> thm list
val positive_numerals: Proof.context -> thm list -> thm list
@@ -33,8 +33,7 @@
AddFunUpdRules |
AddAbsMinMaxRules
- val normalize: config list -> Proof.context -> thm list ->
- Thm.cterm list * thm list
+ val normalize: config list -> Proof.context -> thm list -> cterm list * thm list
val setup: theory -> theory
end
--- a/src/HOL/SMT/Tools/z3_proof.ML Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_proof.ML Tue Oct 27 17:34:00 2009 +0100
@@ -48,7 +48,7 @@
datatype context = Context of {
Ttab: typ Symtab.table,
- ttab: Thm.cterm Symtab.table,
+ ttab: cterm Symtab.table,
etab: T.preterm Inttab.table,
ptab: R.proof Inttab.table,
nctxt: Name.context }
--- a/src/HOL/SMT/Tools/z3_proof_rules.ML Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_proof_rules.ML Tue Oct 27 17:34:00 2009 +0100
@@ -13,7 +13,7 @@
(*proof reconstruction*)
type proof
- val make_proof: rule -> int list -> Thm.cterm * Thm.cterm list -> proof
+ val make_proof: rule -> int list -> cterm * cterm list -> proof
val prove: Proof.context -> thm list option -> proof Inttab.table -> int ->
thm
@@ -103,11 +103,11 @@
Unproved of {
rule: rule,
subs: int list,
- prop: Thm.cterm,
- vars: Thm.cterm list } |
+ prop: cterm,
+ vars: cterm list } |
Sequent of {
- hyps: Thm.cterm list,
- vars: Thm.cterm list,
+ hyps: cterm list,
+ vars: cterm list,
thm: theorem }
fun make_proof r ps (ct, cvs) = Unproved {rule=r, subs=ps, prop=ct, vars=cvs}
--- a/src/HOL/SMT/Tools/z3_proof_terms.ML Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_proof_terms.ML Tue Oct 27 17:34:00 2009 +0100
@@ -6,15 +6,15 @@
signature Z3_PROOF_TERMS =
sig
- val mk_prop: Thm.cterm -> Thm.cterm
- val mk_meta_eq: Thm.cterm -> Thm.cterm -> Thm.cterm
+ val mk_prop: cterm -> cterm
+ val mk_meta_eq: cterm -> cterm -> cterm
type preterm
- val compile: theory -> Name.context -> preterm -> Thm.cterm * Thm.cterm list
+ val compile: theory -> Name.context -> preterm -> cterm * cterm list
val mk_bound: theory -> int -> typ -> preterm
- val mk_fun: Thm.cterm -> preterm list -> preterm
+ val mk_fun: cterm -> preterm list -> preterm
val mk_forall: theory -> string * typ -> preterm -> preterm
val mk_exists: theory -> string * typ -> preterm -> preterm
@@ -73,8 +73,8 @@
datatype preterm = Preterm of {
- cterm: Thm.cterm,
- vars: (int * Thm.cterm) list }
+ cterm: cterm,
+ vars: (int * cterm) list }
fun mk_preterm (ct, vs) = Preterm {cterm=ct, vars=vs}
fun dest_preterm (Preterm {cterm, vars}) = (cterm, vars)
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Tue Oct 27 17:34:00 2009 +0100
@@ -74,7 +74,7 @@
val get_rec_types : descr -> (string * sort) list -> typ list
val interpret_construction : descr -> (string * sort) list
-> { atyp: typ -> 'a, dtyp: typ list -> int * bool -> string * typ list -> 'a }
- -> ((string * Term.typ list) * (string * 'a list) list) list
+ -> ((string * typ list) * (string * 'a list) list) list
val check_nonempty : descr list -> unit
val unfold_datatypes :
theory -> descr -> (string * sort) list -> info Symtab.table ->
--- a/src/HOL/Tools/metis_tools.ML Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/Tools/metis_tools.ML Tue Oct 27 17:34:00 2009 +0100
@@ -589,7 +589,7 @@
(* ------------------------------------------------------------------------- *)
type logic_map =
- {axioms : (Metis.Thm.thm * Thm.thm) list,
+ {axioms : (Metis.Thm.thm * thm) list,
tfrees : ResClause.type_literal list};
fun const_in_metis c (pred, tm_list) =
--- a/src/HOL/Tools/prop_logic.ML Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/Tools/prop_logic.ML Tue Oct 27 17:34:00 2009 +0100
@@ -37,9 +37,9 @@
val eval : (int -> bool) -> prop_formula -> bool (* semantics *)
(* propositional representation of HOL terms *)
- val prop_formula_of_term : Term.term -> int Termtab.table -> prop_formula * int Termtab.table
+ val prop_formula_of_term : term -> int Termtab.table -> prop_formula * int Termtab.table
(* HOL term representation of propositional formulae *)
- val term_of_prop_formula : prop_formula -> Term.term
+ val term_of_prop_formula : prop_formula -> term
end;
structure PropLogic : PROP_LOGIC =
--- a/src/HOL/Tools/quickcheck_generators.ML Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML Tue Oct 27 17:34:00 2009 +0100
@@ -8,7 +8,7 @@
type seed = Random_Engine.seed
val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
-> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
- -> seed -> (('a -> 'b) * (unit -> Term.term)) * seed
+ -> seed -> (('a -> 'b) * (unit -> term)) * seed
val ensure_random_typecopy: string -> theory -> theory
val random_aux_specification: string -> string -> term list -> local_theory -> local_theory
val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list
--- a/src/HOL/Tools/refute.ML Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/Tools/refute.ML Tue Oct 27 17:34:00 2009 +0100
@@ -25,16 +25,15 @@
exception MAXVARS_EXCEEDED
- val add_interpreter : string -> (theory -> model -> arguments -> Term.term ->
+ val add_interpreter : string -> (theory -> model -> arguments -> term ->
(interpretation * model * arguments) option) -> theory -> theory
- val add_printer : string -> (theory -> model -> Term.typ ->
- interpretation -> (int -> bool) -> Term.term option) -> theory -> theory
+ val add_printer : string -> (theory -> model -> typ ->
+ interpretation -> (int -> bool) -> term option) -> theory -> theory
- val interpret : theory -> model -> arguments -> Term.term ->
+ val interpret : theory -> model -> arguments -> term ->
(interpretation * model * arguments)
- val print : theory -> model -> Term.typ -> interpretation ->
- (int -> bool) -> Term.term
+ val print : theory -> model -> typ -> interpretation -> (int -> bool) -> term
val print_model : theory -> model -> (int -> bool) -> string
(* ------------------------------------------------------------------------- *)
@@ -46,10 +45,10 @@
val get_default_params : theory -> (string * string) list
val actual_params : theory -> (string * string) list -> params
- val find_model : theory -> params -> Term.term -> bool -> unit
+ val find_model : theory -> params -> term -> bool -> unit
(* tries to find a model for a formula: *)
- val satisfy_term : theory -> (string * string) list -> Term.term -> unit
+ val satisfy_term : theory -> (string * string) list -> term -> unit
(* tries to find a model that refutes a formula: *)
val refute_term : theory -> (string * string) list -> term -> unit
val refute_goal : theory -> (string * string) list -> thm -> int -> unit
@@ -60,20 +59,18 @@
(* Additional functions used by Nitpick (to be factored out) *)
(* ------------------------------------------------------------------------- *)
- val close_form : Term.term -> Term.term
- val get_classdef : theory -> string -> (string * Term.term) option
- val norm_rhs : Term.term -> Term.term
- val get_def : theory -> string * Term.typ -> (string * Term.term) option
- val get_typedef : theory -> Term.typ -> (string * Term.term) option
- val is_IDT_constructor : theory -> string * Term.typ -> bool
- val is_IDT_recursor : theory -> string * Term.typ -> bool
- val is_const_of_class: theory -> string * Term.typ -> bool
- val monomorphic_term : Type.tyenv -> Term.term -> Term.term
- val specialize_type : theory -> (string * Term.typ) -> Term.term -> Term.term
- val string_of_typ : Term.typ -> string
- val typ_of_dtyp :
- Datatype.descr -> (Datatype.dtyp * Term.typ) list -> Datatype.dtyp
- -> Term.typ
+ val close_form : term -> term
+ val get_classdef : theory -> string -> (string * term) option
+ val norm_rhs : term -> term
+ val get_def : theory -> string * typ -> (string * term) option
+ val get_typedef : theory -> typ -> (string * term) option
+ val is_IDT_constructor : theory -> string * typ -> bool
+ val is_IDT_recursor : theory -> string * typ -> bool
+ val is_const_of_class: theory -> string * typ -> bool
+ val monomorphic_term : Type.tyenv -> term -> term
+ val specialize_type : theory -> (string * typ) -> term -> term
+ val string_of_typ : typ -> string
+ val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
end; (* signature REFUTE *)
structure Refute : REFUTE =
@@ -185,7 +182,7 @@
(* ------------------------------------------------------------------------- *)
type model =
- (Term.typ * int) list * (Term.term * interpretation) list;
+ (typ * int) list * (term * interpretation) list;
(* ------------------------------------------------------------------------- *)
(* arguments: additional arguments required during interpretation of terms *)
@@ -207,10 +204,10 @@
structure RefuteData = TheoryDataFun
(
type T =
- {interpreters: (string * (theory -> model -> arguments -> Term.term ->
+ {interpreters: (string * (theory -> model -> arguments -> term ->
(interpretation * model * arguments) option)) list,
- printers: (string * (theory -> model -> Term.typ -> interpretation ->
- (int -> bool) -> Term.term option)) list,
+ printers: (string * (theory -> model -> typ -> interpretation ->
+ (int -> bool) -> term option)) list,
parameters: string Symtab.table};
val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
val copy = I;
--- a/src/HOL/Tools/res_reconstruct.ML Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML Tue Oct 27 17:34:00 2009 +0100
@@ -10,17 +10,17 @@
val fix_sorts: sort Vartab.table -> term -> term
val invert_const: string -> string
val invert_type_const: string -> string
- val num_typargs: Context.theory -> string -> int
+ val num_typargs: theory -> string -> int
val make_tvar: string -> typ
val strip_prefix: string -> string -> string option
- val setup: Context.theory -> Context.theory
+ val setup: theory -> theory
(* extracting lemma list*)
val find_failure: string -> string option
val lemma_list: bool -> string ->
- string * string vector * (int * int) * Proof.context * Thm.thm * int -> string * string list
+ string * string vector * (int * int) * Proof.context * thm * int -> string * string list
(* structured proofs *)
val structured_proof: string ->
- string * string vector * (int * int) * Proof.context * Thm.thm * int -> string * string list
+ string * string vector * (int * int) * Proof.context * thm * int -> string * string list
end;
structure ResReconstruct : RES_RECONSTRUCT =
--- a/src/HOL/Tools/sat_funcs.ML Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/Tools/sat_funcs.ML Tue Oct 27 17:34:00 2009 +0100
@@ -92,8 +92,8 @@
(* ------------------------------------------------------------------------- *)
datatype CLAUSE = NO_CLAUSE
- | ORIG_CLAUSE of Thm.thm
- | RAW_CLAUSE of Thm.thm * (int * Thm.cterm) list;
+ | ORIG_CLAUSE of thm
+ | RAW_CLAUSE of thm * (int * cterm) list;
(* ------------------------------------------------------------------------- *)
(* resolve_raw_clauses: given a non-empty list of raw clauses, we fold *)
--- a/src/Tools/eqsubst.ML Tue Oct 27 17:19:31 2009 +0100
+++ b/src/Tools/eqsubst.ML Tue Oct 27 17:34:00 2009 +0100
@@ -269,7 +269,7 @@
(* FOR DEBUGGING...
type trace_subst_errT = int (* subgoal *)
* thm (* thm with all goals *)
- * (Thm.cterm list (* certified free var placeholders for vars *)
+ * (cterm list (* certified free var placeholders for vars *)
* thm) (* trivial thm of goal concl *)
(* possible matches/unifiers *)
* thm (* rule *)