src/Pure/section_utils.ML

-(*  Title: 	Pure/section-utils
+(*  Title: 	Pure/section_utils.ML
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
-Utilities for writing new theory sections
+Utilities for writing new theory sections.
 *)
 
 fun ap t u = t$u;
 fun app t (u1,u2) = t $ u1 $ u2;
 
 (*Make distinct individual variables a1, a2, a3, ..., an. *)
 fun mk_frees a [] = []
   | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
 
-(*Make a definition lhs==rhs*)
-fun mk_defpair (lhs, rhs) = 
-  let val Const(name, _) = head_of lhs
-  in (Sign.base_name name ^ "_def", Logic.mk_equals (lhs, rhs)) end;
-
-fun get_def thy s = get_axiom thy (s^"_def");
-
 
 (*Read an assumption in the given theory*)
-fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
+fun assume_read thy a = Thm.assume (read_cterm (sign_of thy) (a,propT));
 
 (*Read a term from string "b", with expected type T*)
 fun readtm sign T b = 
     read_cterm sign (b,T) |> term_of
     handle ERROR => error ("The error(s) above occurred for " ^ b);

 	   then front @ escape (tl (snd (take_prefix Symbol.is_blank rest)))
 	   else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
 
 (*Remove the first and last charaters -- presumed to be quotes*)
 val trim = implode o escape o rev o tl o rev o tl o Symbol.explode;
-
-
-(*Check for some named theory*)
-fun require_thy thy name sect =
-  if exists (equal name) (Sign.stamp_names_of (sign_of thy)) then ()
-  else error ("Need theory " ^ quote name ^ " as an ancestor for " ^ sect);