# HG changeset patch
# User wenzelm
# Date 928518686 -7200
# Node ID 26d64339c25a3e75110ae7fad3957052a5401a77
# Parent  99797f2652d1290a741f4a0bbf6d0d72738c8183
added dest_main_statement;

diff -r 99797f2652d1 -r 26d64339c25a src/Pure/object_logic.ML
--- a/src/Pure/object_logic.ML	Fri Jun 04 19:51:04 1999 +0200
+++ b/src/Pure/object_logic.ML	Fri Jun 04 19:51:26 1999 +0200
@@ -11,6 +11,7 @@
 signature OBJECT_LOGIC =
 sig
   val dest_statement: string * term -> (string * term) list
+  val dest_main_statement: term -> term
   val setup: (theory -> theory) list
 end;
 
@@ -24,6 +25,11 @@
       (case concl of Const ("Trueprop", _) $ t => [(name, t)] | _ => [])
   end;
 
+fun dest_main_statement t =
+  (case Logic.strip_imp_concl t of
+    _ $ t => t
+  | _ => raise TERM ("dest_main", [t]));
+
 
 (* FIXME *)
 val setup = [];