# HG changeset patch
# User paulson
# Date 903597959 -7200
# Node ID bc9748ad849104efaf030428bbce373ca5603720
# Parent  d7927fc7170d9068dc686b0c93290bdeece1be45
Now qed_spec_mp respects locales, by calling ml_store_thm
instead of bind_thm

diff -r d7927fc7170d -r bc9748ad8491 src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Wed Aug 19 17:05:00 1998 +0200
+++ b/src/HOL/HOL.ML	Thu Aug 20 09:25:59 1998 +0200
@@ -393,13 +393,13 @@
   | _ => raise THM("RSmp",0,[th]));
 
 fun normalize_thm funs =
-let fun trans [] th = th
-      | trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
-in trans funs end;
+  let fun trans [] th = th
+	| trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
+  in zero_var_indexes o trans funs end;
 
 fun qed_spec_mp name =
   let val thm = normalize_thm [RSspec,RSmp] (result())
-  in bind_thm(name, thm) end;
+  in ml_store_thm(name, thm) end;
 
 fun qed_goal_spec_mp name thy s p = 
 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
diff -r d7927fc7170d -r bc9748ad8491 src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Wed Aug 19 17:05:00 1998 +0200
+++ b/src/Pure/Thy/thm_database.ML	Thu Aug 20 09:25:59 1998 +0200
@@ -7,6 +7,7 @@
 
 signature THM_DATABASE =
 sig
+  val ml_store_thm: string * thm -> unit
   val store_thm: string * thm -> thm
   val qed_thm: thm option ref
   val bind_thm: string * thm -> unit