--- a/src/Pure/sign.ML Tue Aug 14 13:20:17 2007 +0200
+++ b/src/Pure/sign.ML Tue Aug 14 13:20:18 2007 +0200
@@ -484,7 +484,7 @@
let val ((lhs, rhs), _) = tm
|> no_vars pp
|> Logic.strip_imp_concl
- |> Logic.dest_def pp Term.is_Const (K false) (K false)
+ |> PrimitiveDefs.dest_def pp Term.is_Const (K false) (K false)
in (Term.dest_Const (Term.head_of lhs), rhs) end
handle TERM (msg, _) => error msg;
@@ -500,7 +500,7 @@
fun read_sort' syn ctxt str =
let
val thy = ProofContext.theory_of ctxt;
- val S = Syntax.read_sort ctxt syn (intern_sort thy) str;
+ val S = Syntax.standard_read_sort ctxt syn (intern_sort thy) str;
in certify_sort thy S handle TYPE (msg, _, _) => error msg end;
fun read_sort thy str = read_sort' (syn_of thy) (ProofContext.init thy) str;
@@ -546,7 +546,7 @@
let
val thy = ProofContext.theory_of ctxt;
val T = intern_tycons thy
- (Syntax.read_typ ctxt syn (get_sort thy def_sort) (intern_sort thy) str);
+ (Syntax.standard_read_typ ctxt syn (get_sort thy def_sort) (intern_sort thy) str);
in cert thy T handle TYPE (msg, _, _) => error msg end
handle ERROR msg => cat_error msg ("The error(s) above occurred in type " ^ quote str);
@@ -626,7 +626,7 @@
(*read term*)
val map_const = try (#1 o Term.dest_Const o Consts.read_const consts);
- fun read T = disambig T o Syntax.read_term (get_sort thy def_sort) map_const map_free
+ fun read T = disambig T o Syntax.standard_read_term (get_sort thy def_sort) map_const map_free
(intern_tycons thy) (intern_sort thy) ctxt is_logtype syn T;
in
raw_args