# HG changeset patch # User wenzelm # Date 1213808103 -7200 # Node ID 0ea8e825a1b353a7ee24740885b77676f62e5cfc # Parent 0f8106808e66136fa6b83ea190265f1866464523 removed obsolete read_def_cterms/read_cterm; diff -r 0f8106808e66 -r 0ea8e825a1b3 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Wed Jun 18 18:55:02 2008 +0200 +++ b/src/Pure/more_thm.ML Wed Jun 18 18:55:03 2008 +0200 @@ -46,11 +46,6 @@ val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm val no_attributes: 'a -> 'a * 'b list val simple_fact: 'a -> ('a * 'b list) list - val read_def_cterms: - theory * (indexname -> typ option) * (indexname -> sort option) -> - string list -> bool -> (string * typ)list - -> cterm list * (indexname * typ)list - val read_cterm: theory -> string * typ -> cterm val elim_implies: thm -> thm -> thm val forall_elim_var: int -> thm -> thm val forall_elim_vars: int -> thm -> thm @@ -210,21 +205,6 @@ fun simple_fact x = [(x, [])]; -(** read/certify terms (obsolete) **) (*exception ERROR*) - -fun read_def_cterms (thy, types, sorts) used freeze sTs = - let - val (ts', tye) = Sign.read_def_terms (thy, types, sorts) used freeze sTs; - val cts = map (Thm.cterm_of thy) ts' - handle TYPE (msg, _, _) => error msg - | TERM (msg, _) => error msg; - in (cts, tye) end; - -fun read_cterm thy sT = - let val ([ct], _) = read_def_cterms (thy, K NONE, K NONE) [] true [sT] - in ct end; - - (** basic derived rules **)