--- 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
--- 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
--- 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
--- 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);
(*---------------------------------------------------------------------------