# 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 **)