--- a/src/ZF/ind_syntax.ML Tue Jan 18 15:57:40 1994 +0100
+++ b/src/ZF/ind_syntax.ML Tue Jan 18 16:37:12 1994 +0100
@@ -93,15 +93,15 @@
(*Prove a goal stated as a term, with exception handling*)
fun prove_term sign defs (P,tacsf) =
- let val ct = Sign.cterm_of sign P
+ let val ct = cterm_of sign P
in prove_goalw_cterm defs ct tacsf
handle e => (writeln ("Exception in proof of\n" ^
- Sign.string_of_cterm ct);
+ string_of_cterm ct);
raise e)
end;
(*Read an assumption in the given theory*)
-fun assume_read thy a = assume (Sign.read_cterm (sign_of thy) (a,propT));
+fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
(*Make distinct individual variables a1, a2, a3, ..., an. *)
fun mk_frees a [] = []