Moved some functions which used to be part of thy_data.ML

--- a/src/HOL/HOL.ML	Wed Aug 06 01:12:03 1997 +0200
+++ b/src/HOL/HOL.ML	Wed Aug 06 01:13:46 1997 +0200
@@ -349,7 +349,7 @@
      _ $ (Const("op -->",_)$_$_) => th RS mp
   | _ => raise THM("RSmp",0,[th]));
 
-(*Used in qed_spec_mp, etc., which are declared in thy_data.ML*)
+(*Used in qed_spec_mp, etc.*)
 fun normalize_thm funs =
 let fun trans [] th = th
       | trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
@@ -357,6 +357,15 @@
 
 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));
 
 (*Thus, assignments to the references claset and simpset are recorded
   with theory "HOL".  These files cannot be loaded directly in ROOT.ML.*)

--- a/src/HOL/cladata.ML	Wed Aug 06 01:12:03 1997 +0200
+++ b/src/HOL/cladata.ML	Wed Aug 06 01:13:46 1997 +0200
@@ -59,6 +59,11 @@
      ("claset", ThyMethods {merge = merge, put = put, get = get})
 end;
 
+fun claset_of tname =
+  case get_thydata tname "claset" of
+      None => empty_cs
+    | Some (CS_DATA cs) => cs;
+
 claset := HOL_cs;
 
 (*Better then ex1E for classical reasoner: needs no quantifier duplication!*)

--- a/src/HOL/datatype.ML	Wed Aug 06 01:12:03 1997 +0200
+++ b/src/HOL/datatype.ML	Wed Aug 06 01:13:46 1997 +0200
@@ -5,6 +5,91 @@
    Copyright 1995 TU Muenchen
 *)
 
+(** Information about datatypes **)
+
+(* Retrieve information for a specific datatype *)
+fun datatype_info thy tname =
+  case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of
+      None => None
+    | Some (DT_DATA ds) => assoc (ds, tname);
+
+fun match_info thy tname =
+  case datatype_info thy tname of
+      Some {case_const, constructors, ...} =>
+        {case_const=case_const, constructors=constructors}
+    | None => error ("No datatype \"" ^ tname ^ "\" defined in this theory.");
+
+fun induct_info thy tname =
+  case datatype_info thy tname of
+      Some {constructors, nchotomy, ...} =>
+        {constructors=constructors, nchotomy=nchotomy}
+    | None => error ("No datatype \"" ^ tname ^ "\" defined in this theory.");
+
+
+(* Retrieve information for all datatypes defined in a theory and its
+   ancestors *)
+fun extract_info thy =
+  let val (congs, rewrites) =
+        case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of
+            None => ([], [])
+          | Some (DT_DATA ds) =>
+              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;
+
+local
+
+fun find_tname var Bi =
+  let val frees = map dest_Free (term_frees Bi)
+      val params = Logic.strip_params Bi;
+  in case assoc (frees@params, var) of
+       None => error("No such variable in subgoal: " ^ quote var)
+     | Some(Type(tn,_)) => tn
+     | _ => error("Cannot induct on type of " ^ quote var)
+  end;
+
+fun get_dt_info sign tn =
+      case get_thydata (thyname_of_sign sign) "datatypes" of
+        None => error ("No such datatype: " ^ quote tn)
+      | Some (DT_DATA ds) =>
+          case assoc (ds, tn) of
+            Some info => info
+          | None => error ("Not a datatype: " ^ quote tn)
+
+fun infer_tname state sign i aterm =
+let val (_, _, Bi, _) = dest_state (state, i)
+    val params = Logic.strip_params Bi	        (*params of subgoal i*)
+    val params = rev(rename_wrt_term Bi params) (*as they are printed*)
+    val (types,sorts) = types_sorts state
+    fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
+      | types'(ixn) = types ixn;
+    val (ct,_) = read_def_cterm (sign,types',sorts) [] false
+                                (aterm,TVar(("",0),[]));
+in case #T(rep_cterm ct) of
+     Type(tn,_) => tn
+   | _ => error("Cannot induct on type of " ^ quote aterm)
+end;
+
+in
+
+(* generic induction tactic for datatypes *)
+fun induct_tac var i state = state |>
+        let val (_, _, Bi, _) = dest_state (state, i)
+            val sign = #sign(rep_thm state)
+            val tn = find_tname var Bi
+            val ind_tac = #induct_tac(get_dt_info sign tn)
+        in ind_tac var i end;
+
+(* generic exhaustion tactic for datatypes *)
+fun exhaust_tac aterm i state = state |>
+        let val sign = #sign(rep_thm state)
+            val tn = infer_tname state sign i aterm
+            val exh_tac = #exhaust_tac(get_dt_info sign tn)
+        in exh_tac aterm i end;
+
+end;
+
+
 (* should go into Pure *)
 fun ALLNEWSUBGOALS tac tacf i st0 = st0 |>
   (tac i THEN

--- a/src/HOL/simpdata.ML	Wed Aug 06 01:12:03 1997 +0200
+++ b/src/HOL/simpdata.ML	Wed Aug 06 01:13:46 1997 +0200
@@ -401,6 +401,11 @@
      ("simpset", ThyMethods {merge = merge, put = put, get = get})
 end;
 
+fun simpset_of tname =
+  case get_thydata tname "simpset" of
+      None => empty_ss
+    | Some (SS_DATA ss) => ss;
+
 type dtype_info = {case_const:term,
                    case_rewrites:thm list,
                    constructors:term list,
@@ -426,10 +431,6 @@
 end;
 
 
-add_thy_reader_file "thy_data.ML";
-
-
-
 
 (*** Integration of simplifier with classical reasoner ***)