# HG changeset patch
# User wenzelm
# Date 921687636 -3600
# Node ID e70ae9b575cc2bc33357e17836e3335f4f60fe80
# Parent  fee481d8ea7ac086240943edf43740f6e5ec5792
Theory.sign_of;

diff -r fee481d8ea7a -r e70ae9b575cc TFL/dcterm.sml
--- a/TFL/dcterm.sml	Wed Mar 17 17:19:18 1999 +0100
+++ b/TFL/dcterm.sml	Wed Mar 17 17:20:36 1999 +0100
@@ -61,7 +61,7 @@
  *---------------------------------------------------------------------------*)
 
 fun mk_const sign pr = cterm_of sign (Const pr);
-val mk_hol_const = mk_const (sign_of HOL.thy);
+val mk_hol_const = mk_const (Theory.sign_of HOL.thy);
 
 fun mk_exists (r as (Bvar,Body)) = 
   let val ty = #T(rep_cterm Bvar)
@@ -181,7 +181,7 @@
 (*---------------------------------------------------------------------------
  * Going into and out of prop
  *---------------------------------------------------------------------------*)
-local val prop = cterm_of (sign_of HOL.thy) (read"Trueprop")
+local val prop = cterm_of (Theory.sign_of HOL.thy) (read"Trueprop")
 in fun mk_prop ctm =
      case (#t(rep_cterm ctm))
        of (Const("Trueprop",_)$_) => ctm
diff -r fee481d8ea7a -r e70ae9b575cc TFL/post.sml
--- a/TFL/post.sml	Wed Mar 17 17:19:18 1999 +0100
+++ b/TFL/post.sml	Wed Mar 17 17:20:36 1999 +0100
@@ -56,7 +56,7 @@
   case termination_goals rules of
       [] => error "tgoalw: no termination conditions to prove"
     | L  => goalw_cterm defs 
-              (cterm_of (sign_of thy) 
+              (Thm.cterm_of (Theory.sign_of thy) 
 	                (HOLogic.mk_Trueprop(USyntax.list_mk_conj L)));
 
 fun tgoal thy = tgoalw thy [];
@@ -92,7 +92,7 @@
 (*lcp's version: takes strings; doesn't return "thm" 
         (whose signature is a draft and therefore useless) *)
 fun define thy fid R eqs = 
-  let fun read thy = readtm (sign_of thy) (TVar(("DUMMY",0),[])) 
+  let fun read thy = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[])) 
   in  define_i thy fid (read thy R) (map (read thy) eqs)  end
   handle Utils.ERR {mesg,...} => error mesg;
 
@@ -194,7 +194,7 @@
 val defaultTflCongs = eq_reflect_list [Thms.LET_CONG, if_cong];
 
 fun simplify_defn (ss, tflCongs) (thy,(id,pats)) =
-   let val dummy = deny (id mem (Sign.stamp_names_of (sign_of thy)))
+   let val dummy = deny (id mem (Sign.stamp_names_of (Theory.sign_of thy)))
                         ("Recursive definition " ^ id ^ 
                          " would clash with the theory of the same name!")
        val def =  freezeT(get_def thy id)   RS   meta_eq_to_obj_eq
diff -r fee481d8ea7a -r e70ae9b575cc TFL/tfl.sml
--- a/TFL/tfl.sml	Wed Mar 17 17:19:18 1999 +0100
+++ b/TFL/tfl.sml	Wed Mar 17 17:20:36 1999 +0100
@@ -336,7 +336,7 @@
 	                  (wfrec $ map_term_types poly_tvars R) 
 	              $ functional
      val (def_term, _) = 
-	 Sign.infer_types (sign_of thy) (K None) (K None) [] false
+	 Sign.infer_types (Theory.sign_of thy) (K None) (K None) [] false
 	       ([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M], 
 		propT)
   in  PureThy.add_defs_i [Thm.no_attributes (def_name, def_term)] thy  end
diff -r fee481d8ea7a -r e70ae9b575cc TFL/thry.sml
--- a/TFL/thry.sml	Wed Mar 17 17:19:18 1999 +0100
+++ b/TFL/thry.sml	Wed Mar 17 17:20:36 1999 +0100
@@ -19,13 +19,13 @@
       fun tmbind (x,y) = (Var  (x,type_of y), y)
 in
  fun match_term thry pat ob = 
-    let val tsig = #tsig(Sign.rep_sg(sign_of thry))
+    let val tsig = #tsig(Sign.rep_sg(Theory.sign_of thry))
         val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)
     in (map tmbind tm_theta, map tybind ty_theta)
     end
 
  fun match_type thry pat ob = 
-    map tybind(Type.typ_match (#tsig(Sign.rep_sg(sign_of thry))) ([],(pat,ob)))
+    map tybind(Type.typ_match (#tsig(Sign.rep_sg(Theory.sign_of thry))) ([],(pat,ob)))
 end;
 
 
@@ -33,7 +33,7 @@
  * Typing 
  *---------------------------------------------------------------------------*)
 
-fun typecheck thry = cterm_of (sign_of thry);
+fun typecheck thry = Thm.cterm_of (Theory.sign_of thry);
 
 
 (*---------------------------------------------------------------------------