# HG changeset patch
# User wenzelm
# Date 1255734359 -7200
# Node ID 23a8c5ac35f8175e7fb10e5d29a7e3b2200ab339
# Parent  3228627994d94cdcd3f1234148ec11da58a59aed
removed obsolete old goal command;

diff -r 3228627994d9 -r 23a8c5ac35f8 src/HOL/Tools/TFL/post.ML
--- a/src/HOL/Tools/TFL/post.ML	Sat Oct 17 00:53:18 2009 +0200
+++ b/src/HOL/Tools/TFL/post.ML	Sat Oct 17 01:05:59 2009 +0200
@@ -7,8 +7,6 @@
 
 signature TFL =
 sig
-  val tgoalw: theory -> thm list -> thm list -> thm list
-  val tgoal: theory -> thm list -> thm list
   val define_i: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring ->
     term -> term list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list}
   val define: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring ->
@@ -33,19 +31,6 @@
       (List.foldr (fn (th,A) => gen_union (op aconv) (prems_of th, A)) [] rules);
 
 (*---------------------------------------------------------------------------
- * Finds the termination conditions in (highly massaged) definition and
- * puts them into a goalstack.
- *--------------------------------------------------------------------------*)
-fun tgoalw thy defs rules =
-  case termination_goals rules of
-      [] => error "tgoalw: no termination conditions to prove"
-    | L  => OldGoals.goalw_cterm defs
-              (Thm.cterm_of thy
-                        (HOLogic.mk_Trueprop(USyntax.list_mk_conj L)));
-
-fun tgoal thy = tgoalw thy [];
-
-(*---------------------------------------------------------------------------
  * Three postprocessors are applied to the definition.  It
  * attempts to prove wellfoundedness of the given relation, simplifies the
  * non-proved termination conditions, and finally attempts to prove the