# HG changeset patch
# User wenzelm
# Date 1140035704 -3600
# Node ID 358c0eb6d78553b7f7000995bf70171455934673
# Parent  113dbd65319ed716fe78c905c3435f75e3e5252b
chop is no longer pervasive;
removed obsolete thms_containing;

diff -r 113dbd65319e -r 358c0eb6d785 src/Pure/old_goals.ML
--- a/src/Pure/old_goals.ML	Wed Feb 15 21:35:02 2006 +0100
+++ b/src/Pure/old_goals.ML	Wed Feb 15 21:35:04 2006 +0100
@@ -31,7 +31,6 @@
   val by: tactic -> unit
   val back: unit -> unit
   val choplev: int -> unit
-  val chop: unit -> unit
   val undo: unit -> unit
   val bind_thm: string * thm -> unit
   val bind_thms: string * thm list -> unit
@@ -44,7 +43,6 @@
   val qed_goalw_spec_mp: string -> theory -> thm list -> string
     -> (thm list -> tactic list) -> unit
   val no_qed: unit -> unit
-  val thms_containing: xstring list -> (string * thm) list
 end;
 
 signature OLD_GOALS =
@@ -52,6 +50,7 @@
   include GOALS
   val legacy: bool ref
   type proof
+  val chop: unit -> unit
   val reset_goals: unit -> unit
   val result_error_fn: (thm -> string -> thm) ref
   val print_sign_exn: theory -> exn -> 'a
@@ -502,9 +501,7 @@
 fun fa() = by (FIRSTGOAL (trace_goalno_tac assume_tac));
 
 
-(** theorem database operations **)
-
-(* store *)
+(** theorem database **)
 
 fun bind_thm (name, thm) = ThmDatabase.ml_store_thm (name, standard thm);
 fun bind_thms (name, thms) = ThmDatabase.ml_store_thms (name, map standard thms);
@@ -522,20 +519,6 @@
 
 fun no_qed () = ();
 
-
-(* retrieve *)
-
-fun thms_containing raw_consts =
-  let
-    val thy = Thm.theory_of_thm (topthm ());
-    val consts = map (Sign.intern_const thy) raw_consts;
-  in
-    (case List.filter (is_none o Sign.const_type thy) consts of
-      [] => ()
-    | cs => error ("thms_containing: undeclared consts " ^ commas_quote cs));
-    PureThy.thms_containing_consts thy consts
-  end;
-
 end;
 
 structure Goals: GOALS = OldGoals;