# HG changeset patch
# User paulson
# Date 1115743063 -7200
# Node ID fd02dd265b783f40a03029bc24fa81f09d1448a0
# Parent  d97c12a4f31b72c77ed879fdbc8f3e6a3f79dd34
new cterm primitives

diff -r d97c12a4f31b -r fd02dd265b78 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue May 10 10:25:21 2005 +0200
+++ b/src/Pure/drule.ML	Tue May 10 18:37:43 2005 +0200
@@ -86,8 +86,10 @@
 signature DRULE =
 sig
   include BASIC_DRULE
+  val list_comb: cterm * cterm list -> cterm
   val strip_comb: cterm -> cterm * cterm list
   val strip_type: ctyp -> ctyp list * ctyp
+  val beta_conv: cterm -> cterm -> cterm
   val plain_prop_of: thm -> term
   val add_used: thm -> string list -> string list
   val rule_attribute: ('a -> thm -> thm) -> 'a attribute
@@ -206,6 +208,10 @@
 fun list_implies([], B) = B
   | list_implies(A::AS, B) = mk_implies (A, list_implies(AS,B));
 
+(*cterm version of list_comb: maps  (f, [t1,...,tn])  to  f(t1,...,tn) *)
+fun list_comb (f, []) = f
+  | list_comb (f, t::ts) = list_comb (Thm.capply f t, ts);
+
 (*cterm version of strip_comb: maps  f(t1,...,tn)  to  (f, [t1,...,tn]) *)
 fun strip_comb ct = 
   let
@@ -223,6 +229,11 @@
       in (cT1 :: cTs, cT') end
   | _ => ([], cT));
 
+(*Beta-conversion for cterms, where x is an abstraction. Simply returns the rhs
+  of the meta-equality returned by the beta_conversion rule.*)
+fun beta_conv x y = 
+    #2 (Thm.dest_comb (cprop_of (Thm.beta_conversion false (Thm.capply x y))));
+
 fun plain_prop_of raw_thm =
   let
     val thm = Thm.strip_shyps raw_thm;
@@ -287,7 +298,8 @@
 fun types_sorts thm =
     let val {prop, hyps, tpairs, ...} = Thm.rep_thm thm;
         (* bogus term! *)
-        val big = list_comb (list_comb (prop, hyps), Thm.terms_of_tpairs tpairs);
+        val big = Term.list_comb 
+                    (Term.list_comb (prop, hyps), Thm.terms_of_tpairs tpairs);
         val vars = map dest_Var (term_vars big);
         val frees = map dest_Free (term_frees big);
         val tvars = term_tvars big;