# HG changeset patch
# User wenzelm
# Date 875720552 -7200
# Node ID 8e1794c4e81b997ed4632f1fd6750e7df85a9072
# Parent  6a4f3b976db3fb706f22bd56951055915b53529a
moved theory stuff (add_defs etc.) to theory.ML;

diff -r 6a4f3b976db3 -r 8e1794c4e81b src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Oct 01 17:41:20 1997 +0200
+++ b/src/Pure/drule.ML	Wed Oct 01 17:42:32 1997 +0200
@@ -3,15 +3,13 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Derived rules and other operations on theorems and theories
+Derived rules and other operations on theorems.
 *)
 
 infix 0 RS RSN RL RLN MRS MRL COMP;
 
 signature DRULE =
-  sig
-  val add_defs		: (string * string) list -> theory -> theory
-  val add_defs_i	: (string * term) list -> theory -> theory
+sig
   val asm_rl		: thm
   val assume_ax		: theory -> string -> thm
   val COMP		: thm * thm -> thm
@@ -68,134 +66,12 @@
   val triv_forall_equality: thm
   val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
   val zero_var_indexes	: thm -> thm
-  end;
+end;
 
 
 structure Drule : DRULE =
 struct
 
-(**** Extend Theories ****)
-
-(** add constant definitions **)
-
-(* all_axioms_of *)
-
-(*results may contain duplicates!*)
-
-fun ancestry_of thy =
-  thy :: List.concat (map ancestry_of (parents_of thy));
-
-val all_axioms_of =
-  List.concat o map (Symtab.dest o #new_axioms o rep_theory) o ancestry_of;
-
-
-(* clash_types, clash_consts *)
-
-(*check if types have common instance (ignoring sorts)*)
-
-fun clash_types ty1 ty2 =
-  let
-    val ty1' = Type.varifyT ty1;
-    val ty2' = incr_tvar (maxidx_of_typ ty1' + 1) (Type.varifyT ty2);
-  in
-    Type.raw_unify (ty1', ty2')
-  end;
-
-fun clash_consts (c1, ty1) (c2, ty2) =
-  c1 = c2 andalso clash_types ty1 ty2;
-
-
-(* clash_defns *)
-
-fun clash_defn c_ty (name, tm) =
-  let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals tm))) in
-    if clash_consts c_ty (c, ty') then Some (name, ty') else None
-  end handle TERM _ => None;
-
-fun clash_defns c_ty axms =
-  distinct (mapfilter (clash_defn c_ty) axms);
-
-
-(* dest_defn *)
-
-fun dest_defn tm =
-  let
-    fun err msg = raise_term msg [tm];
-
-    val (lhs, rhs) = Logic.dest_equals (Logic.strip_imp_concl tm)
-      handle TERM _ => err "Not a meta-equality (==)";
-    val (head, args) = strip_comb lhs;
-    val (c, ty) = dest_Const head
-      handle TERM _ => err "Head of lhs not a constant";
-
-    fun occs_const (Const c_ty') = (c_ty' = (c, ty))
-      | occs_const (Abs (_, _, t)) = occs_const t
-      | occs_const (t $ u) = occs_const t orelse occs_const u
-      | occs_const _ = false;
-
-    val show_frees = commas_quote o map (fst o dest_Free);
-    val show_tfrees = commas_quote o map fst;
-
-    val lhs_dups = duplicates args;
-    val rhs_extras = gen_rems (op =) (term_frees rhs, args);
-    val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty);
-  in
-    if not (forall is_Free args) then
-      err "Arguments (on lhs) must be variables"
-    else if not (null lhs_dups) then
-      err ("Duplicate variables on lhs: " ^ show_frees lhs_dups)
-    else if not (null rhs_extras) then
-      err ("Extra variables on rhs: " ^ show_frees rhs_extras)
-    else if not (null rhs_extrasT) then
-      err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT)
-    else if occs_const rhs then
-      err ("Constant to be defined occurs on rhs")
-    else (c, ty)
-  end;
-
-
-(* check_defn *)
-
-fun err_in_defn name msg =
-  (writeln msg; error ("The error(s) above occurred in definition " ^ quote name));
-
-fun check_defn sign (axms, (name, tm)) =
-  let
-    fun show_const (c, ty) = quote (Pretty.string_of (Pretty.block
-      [Pretty.str (c ^ " ::"), Pretty.brk 1, Sign.pretty_typ sign ty]));
-
-    fun show_defn c (dfn, ty') = show_const (c, ty') ^ " in " ^ dfn;
-    fun show_defns c = cat_lines o map (show_defn c);
-
-    val (c, ty) = dest_defn tm
-      handle TERM (msg, _) => err_in_defn name msg;
-    val defns = clash_defns (c, ty) axms;
-  in
-    if not (null defns) then
-      err_in_defn name ("Definition of " ^ show_const (c, ty) ^
-        "\nclashes with " ^ show_defns c defns)
-    else (name, tm) :: axms
-  end;
-
-
-(* add_defs *)
-
-fun ext_defns prep_axm raw_axms thy =
-  let
-    val axms = map (prep_axm (sign_of thy)) raw_axms;
-    val all_axms = all_axioms_of thy;
-  in
-    foldl (check_defn (sign_of thy)) (all_axms, axms);
-    add_axioms_i axms thy
-  end;
-
-val add_defs_i = ext_defns cert_axm;
-val add_defs = ext_defns read_axm;
-
-
-
-(**** More derived rules and operations on theorems ****)
-
 (** some cterm->cterm operations: much faster than calling cterm_of! **)
 
 (** SAME NAMES as in structure Logic: use compound identifiers! **)