ThmDatabase.ml_store_thm;
authorwenzelm
Wed Feb 03 17:33:20 1999 +0100 (1999-02-03)
changeset 62140513cfd1a598
parent 6213 f5bdd6497e08
child 6215 6165747678ba
ThmDatabase.ml_store_thm;
src/HOL/HOL.ML
     1.1 --- a/src/HOL/HOL.ML	Wed Feb 03 17:32:10 1999 +0100
     1.2 +++ b/src/HOL/HOL.ML	Wed Feb 03 17:33:20 1999 +0100
     1.3 @@ -407,7 +407,7 @@
     1.4  
     1.5  fun qed_spec_mp name =
     1.6    let val thm = normalize_thm [RSspec,RSmp] (result())
     1.7 -  in ml_store_thm(name, thm) end;
     1.8 +  in ThmDatabase.ml_store_thm(name, thm) end;
     1.9  
    1.10  fun qed_goal_spec_mp name thy s p = 
    1.11  	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));