1.1 --- a/src/HOL/HOL.ML	Wed Aug 19 17:05:00 1998 +0200
     1.2 +++ b/src/HOL/HOL.ML	Thu Aug 20 09:25:59 1998 +0200
     1.3 @@ -393,13 +393,13 @@
     1.4    | _ => raise THM("RSmp",0,[th]));
     1.5  
     1.6  fun normalize_thm funs =
     1.7 -let fun trans [] th = th
     1.8 -      | trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
     1.9 -in trans funs end;
    1.10 +  let fun trans [] th = th
    1.11 +	| trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
    1.12 +  in zero_var_indexes o trans funs end;
    1.13  
    1.14  fun qed_spec_mp name =
    1.15    let val thm = normalize_thm [RSspec,RSmp] (result())
    1.16 -  in bind_thm(name, thm) end;
    1.17 +  in ml_store_thm(name, thm) end;
    1.18  
    1.19  fun qed_goal_spec_mp name thy s p = 
    1.20  	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));

     2.1 --- a/src/Pure/Thy/thm_database.ML	Wed Aug 19 17:05:00 1998 +0200
     2.2 +++ b/src/Pure/Thy/thm_database.ML	Thu Aug 20 09:25:59 1998 +0200
     2.3 @@ -7,6 +7,7 @@
     2.4  
     2.5  signature THM_DATABASE =
     2.6  sig
     2.7 +  val ml_store_thm: string * thm -> unit
     2.8    val store_thm: string * thm -> thm
     2.9    val qed_thm: thm option ref
    2.10    val bind_thm: string * thm -> unit