# HG changeset patch
# User wenzelm
# Date 1176564970 -7200
# Node ID 92448396c9d980c53b5ee3d3b827a1008e1cc6d4
# Parent  9d42e5365ad1f4aa45aee5e08ecf77b6210846e6
added read_def_cterms, read_cterm (from thm.ML);

diff -r 9d42e5365ad1 -r 92448396c9d9 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sat Apr 14 17:36:09 2007 +0200
+++ b/src/Pure/more_thm.ML	Sat Apr 14 17:36:10 2007 +0200
@@ -27,14 +27,20 @@
   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
 end;
 
 structure Thm: THM =
 struct
 
-(* compare theorems *)
+(** compare theorems **)
 
-(*order: ignores theory context!*)
+(* order: ignores theory context! *)
+
 fun thm_ord (th1, th2) =
   let
     val {shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} = Thm.rep_thm th1;
@@ -51,6 +57,9 @@
     | ord => ord)
   end;
 
+
+(* equality *)
+
 fun eq_thm ths =
   Context.joinable (pairself Thm.theory_of_thm ths) andalso
   thm_ord ths = EQUAL;
@@ -60,12 +69,15 @@
 val eq_thm_thy = eq_thy o pairself Thm.theory_of_thm;
 val eq_thm_prop = op aconv o pairself Thm.full_prop_of;
 
-(*pattern equivalence*)
+
+(* pattern equivalence *)
+
 fun equiv_thm ths =
   Pattern.equiv (Theory.merge (pairself Thm.theory_of_thm ths)) (pairself Thm.full_prop_of ths);
 
 
-(* theorem kinds *)
+
+(** theorem kinds **)
 
 val axiomK = "axiom";
 val assumptionK = "assumption";
@@ -76,7 +88,8 @@
 val internalK = "internal";
 
 
-(* attributes *)
+
+(** attributes **)
 
 fun rule_attribute f (x, th) = (x, f x th);
 fun declaration_attribute f (x, th) = (f th x, th);
@@ -94,6 +107,21 @@
 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;
+
+
 open Thm;
 
 end;