# HG changeset patch
# User wenzelm
# Date 1187090418 -7200
# Node ID d68040094415b328de587577ec6c509cddf1a0ef
# Parent  c9e05c49d02cf4be086ec78df1273c8a012e645c
PrimitiveDefs.dest_def;
Syntax.standard_read;

diff -r c9e05c49d02c -r d68040094415 src/Pure/sign.ML
--- 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