# HG changeset patch
# User paulson
# Date 854548338 -3600
# Node ID d571d6660240e404265631405a9ffde55d663fef
# Parent  8ef656dbf4fa51b1906910dfff9ccf9f4e804e14
Moved qed_spec_mp, etc., from HOL.ML to thy_data.ML so that they work
properly in children databases

diff -r 8ef656dbf4fa -r d571d6660240 src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Tue Jan 28 16:21:15 1997 +0100
+++ b/src/HOL/HOL.ML	Wed Jan 29 15:32:18 1997 +0100
@@ -313,7 +313,8 @@
 fun stac th = CHANGED o rtac (th RS ssubst);
 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
 
-(** strip proved goal while preserving !-bound var names **)
+
+(** strip ! and --> from proved goal while preserving !-bound var names **)
 
 local
 
@@ -337,21 +338,12 @@
      _ $ (Const("op -->",_)$_$_) => th RS mp
   | _ => raise THM("RSmp",0,[th]));
 
+(*Used in qed_spec_mp, etc., which are declared in thy_data.ML*)
 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;
 
-fun qed_spec_mp name =
-  let val thm = normalize_thm [RSspec,RSmp] (result())
-  in bind_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));
-
-fun qed_goalw_spec_mp name thy defs s p = 
-	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
-
 end;
 
 
diff -r 8ef656dbf4fa -r d571d6660240 src/HOL/thy_data.ML
--- a/src/HOL/thy_data.ML	Tue Jan 28 16:21:15 1997 +0100
+++ b/src/HOL/thy_data.ML	Wed Jan 29 15:32:18 1997 +0100
@@ -48,3 +48,18 @@
               let val info = map snd ds
               in (map #case_cong info, flat (map #case_rewrites info)) end;
   in {case_congs = congs, case_rewrites = rewrites} end;
+
+
+(*Must be redefined in order to refer to the new instance of bind_thm
+  created by init_thy_reader.*)
+
+fun qed_spec_mp name =
+  let val thm = normalize_thm [RSspec,RSmp] (result())
+  in bind_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));
+
+fun qed_goalw_spec_mp name thy defs s p = 
+	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
+