added dest_main_statement;

--- 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 = [];