moved mk_defpair to logic.ML;
authorwenzelm
Wed Apr 29 11:22:01 1998 +0200 (1998-04-29)
changeset 484899c8d95c51d6
parent 4847 ea7d7a65e4e9
child 4849 a9d5b8f8e40f
moved mk_defpair to logic.ML;
moved get_def to thm.ML;
moved require_thy to theory.ML;
src/Pure/section_utils.ML
     1.1 --- a/src/Pure/section_utils.ML	Wed Apr 29 11:20:53 1998 +0200
     1.2 +++ b/src/Pure/section_utils.ML	Wed Apr 29 11:22:01 1998 +0200
     1.3 @@ -1,9 +1,9 @@
     1.4 -(*  Title: 	Pure/section-utils
     1.5 +(*  Title: 	Pure/section_utils.ML
     1.6      ID:         $Id$
     1.7      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1994  University of Cambridge
     1.9  
    1.10 -Utilities for writing new theory sections
    1.11 +Utilities for writing new theory sections.
    1.12  *)
    1.13  
    1.14  fun ap t u = t$u;
    1.15 @@ -13,16 +13,9 @@
    1.16  fun mk_frees a [] = []
    1.17    | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
    1.18  
    1.19 -(*Make a definition lhs==rhs*)
    1.20 -fun mk_defpair (lhs, rhs) = 
    1.21 -  let val Const(name, _) = head_of lhs
    1.22 -  in (Sign.base_name name ^ "_def", Logic.mk_equals (lhs, rhs)) end;
    1.23 -
    1.24 -fun get_def thy s = get_axiom thy (s^"_def");
    1.25 -
    1.26  
    1.27  (*Read an assumption in the given theory*)
    1.28 -fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
    1.29 +fun assume_read thy a = Thm.assume (read_cterm (sign_of thy) (a,propT));
    1.30  
    1.31  (*Read a term from string "b", with expected type T*)
    1.32  fun readtm sign T b = 
    1.33 @@ -65,9 +58,3 @@
    1.34  
    1.35  (*Remove the first and last charaters -- presumed to be quotes*)
    1.36  val trim = implode o escape o rev o tl o rev o tl o Symbol.explode;
    1.37 -
    1.38 -
    1.39 -(*Check for some named theory*)
    1.40 -fun require_thy thy name sect =
    1.41 -  if exists (equal name) (Sign.stamp_names_of (sign_of thy)) then ()
    1.42 -  else error ("Need theory " ^ quote name ^ " as an ancestor for " ^ sect);