src/Pure/drule.ML
 changeset 10767 8fa4aafa7314 parent 10667 75a1c9575edb child 10815 dd5fb02ff872
```--- a/src/Pure/drule.ML	Wed Jan 03 11:14:48 2001 +0100
+++ b/src/Pure/drule.ML	Wed Jan 03 21:18:31 2001 +0100
@@ -123,15 +123,15 @@
fun dest_implies ct =
case term_of ct of
(Const("==>", _) \$ _ \$ _) =>
-            let val (ct1,ct2) = dest_comb ct
-            in  (#2 (dest_comb ct1), ct2)  end
+            let val (ct1,ct2) = Thm.dest_comb ct
+            in  (#2 (Thm.dest_comb ct1), ct2)  end
| _ => raise TERM ("dest_implies", [term_of ct]) ;

fun dest_equals ct =
case term_of ct of
(Const("==", _) \$ _ \$ _) =>
-            let val (ct1,ct2) = dest_comb ct
-            in  (#2 (dest_comb ct1), ct2)  end
+            let val (ct1,ct2) = Thm.dest_comb ct
+            in  (#2 (Thm.dest_comb ct1), ct2)  end
| _ => raise TERM ("dest_equals", [term_of ct]) ;

@@ -151,7 +151,7 @@
(* A1==>...An==>B  goes to B, where B is not an implication *)
fun strip_imp_concl ct =
case term_of ct of (Const("==>", _) \$ _ \$ _) =>
-        strip_imp_concl (#2 (dest_comb ct))
+        strip_imp_concl (#2 (Thm.dest_comb ct))
| _ => ct;

(*The premises of a theorem, as a cterm list*)
@@ -162,7 +162,7 @@
val implies = cterm_of proto_sign Term.implies;

(*cterm version of mk_implies*)
-fun mk_implies(A,B) = capply (capply implies A) B;
+fun mk_implies(A,B) = Thm.capply (Thm.capply implies A) B;

(*cterm version of list_implies: [A1,...,An], B  goes to [|A1;==>;An|]==>B *)
fun list_implies([], B) = B```