chop is no longer pervasive;
authorwenzelm
Wed Feb 15 21:35:04 2006 +0100 (2006-02-15)
changeset 19053358c0eb6d785
parent 19052 113dbd65319e
child 19054 af7cc6063285
chop is no longer pervasive;
removed obsolete thms_containing;
src/Pure/old_goals.ML
     1.1 --- a/src/Pure/old_goals.ML	Wed Feb 15 21:35:02 2006 +0100
     1.2 +++ b/src/Pure/old_goals.ML	Wed Feb 15 21:35:04 2006 +0100
     1.3 @@ -31,7 +31,6 @@
     1.4    val by: tactic -> unit
     1.5    val back: unit -> unit
     1.6    val choplev: int -> unit
     1.7 -  val chop: unit -> unit
     1.8    val undo: unit -> unit
     1.9    val bind_thm: string * thm -> unit
    1.10    val bind_thms: string * thm list -> unit
    1.11 @@ -44,7 +43,6 @@
    1.12    val qed_goalw_spec_mp: string -> theory -> thm list -> string
    1.13      -> (thm list -> tactic list) -> unit
    1.14    val no_qed: unit -> unit
    1.15 -  val thms_containing: xstring list -> (string * thm) list
    1.16  end;
    1.17  
    1.18  signature OLD_GOALS =
    1.19 @@ -52,6 +50,7 @@
    1.20    include GOALS
    1.21    val legacy: bool ref
    1.22    type proof
    1.23 +  val chop: unit -> unit
    1.24    val reset_goals: unit -> unit
    1.25    val result_error_fn: (thm -> string -> thm) ref
    1.26    val print_sign_exn: theory -> exn -> 'a
    1.27 @@ -502,9 +501,7 @@
    1.28  fun fa() = by (FIRSTGOAL (trace_goalno_tac assume_tac));
    1.29  
    1.30  
    1.31 -(** theorem database operations **)
    1.32 -
    1.33 -(* store *)
    1.34 +(** theorem database **)
    1.35  
    1.36  fun bind_thm (name, thm) = ThmDatabase.ml_store_thm (name, standard thm);
    1.37  fun bind_thms (name, thms) = ThmDatabase.ml_store_thms (name, map standard thms);
    1.38 @@ -522,20 +519,6 @@
    1.39  
    1.40  fun no_qed () = ();
    1.41  
    1.42 -
    1.43 -(* retrieve *)
    1.44 -
    1.45 -fun thms_containing raw_consts =
    1.46 -  let
    1.47 -    val thy = Thm.theory_of_thm (topthm ());
    1.48 -    val consts = map (Sign.intern_const thy) raw_consts;
    1.49 -  in
    1.50 -    (case List.filter (is_none o Sign.const_type thy) consts of
    1.51 -      [] => ()
    1.52 -    | cs => error ("thms_containing: undeclared consts " ^ commas_quote cs));
    1.53 -    PureThy.thms_containing_consts thy consts
    1.54 -  end;
    1.55 -
    1.56  end;
    1.57  
    1.58  structure Goals: GOALS = OldGoals;