src/Pure/old_goals.ML
changeset 26414 2780de5a1422
parent 26291 d01bf7b10c75
child 26429 1afbc0139b1b
     1.1 --- a/src/Pure/old_goals.ML	Wed Mar 26 22:40:03 2008 +0100
     1.2 +++ b/src/Pure/old_goals.ML	Wed Mar 26 22:40:05 2008 +0100
     1.3 @@ -30,8 +30,6 @@
     1.4    val back: unit -> unit
     1.5    val choplev: int -> unit
     1.6    val undo: unit -> unit
     1.7 -  val bind_thm: string * thm -> unit
     1.8 -  val bind_thms: string * thm list -> unit
     1.9    val qed: string -> unit
    1.10    val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit
    1.11    val qed_goalw: string -> theory -> thm list -> string
    1.12 @@ -500,17 +498,14 @@
    1.13  fun fa() = by (FIRSTGOAL (trace_goalno_tac assume_tac));
    1.14  
    1.15  
    1.16 -(** theorem database **)
    1.17 -
    1.18 -fun bind_thm (name, thm) = ThmDatabase.ml_store_thm (name, standard thm);
    1.19 -fun bind_thms (name, thms) = ThmDatabase.ml_store_thms (name, map standard thms);
    1.20 +(** theorem bindings **)
    1.21  
    1.22 -fun qed name = ThmDatabase.ml_store_thm (name, result ());
    1.23 -fun qed_goal name thy goal tacsf = ThmDatabase.ml_store_thm (name, prove_goal thy goal tacsf);
    1.24 +fun qed name = ML_Context.ml_store_thm (name, result ());
    1.25 +fun qed_goal name thy goal tacsf = ML_Context.ml_store_thm (name, prove_goal thy goal tacsf);
    1.26  fun qed_goalw name thy rews goal tacsf =
    1.27 -  ThmDatabase.ml_store_thm (name, prove_goalw thy rews goal tacsf);
    1.28 +  ML_Context.ml_store_thm (name, prove_goalw thy rews goal tacsf);
    1.29  fun qed_spec_mp name =
    1.30 -  ThmDatabase.ml_store_thm (name, ObjectLogic.rulify_no_asm (result ()));
    1.31 +  ML_Context.ml_store_thm (name, ObjectLogic.rulify_no_asm (result ()));
    1.32  fun qed_goal_spec_mp name thy s p =
    1.33    bind_thm (name, ObjectLogic.rulify_no_asm (prove_goal thy s p));
    1.34  fun qed_goalw_spec_mp name thy defs s p =