PrimitiveDefs.dest_def;
authorwenzelm
Tue Aug 14 13:20:18 2007 +0200 (2007-08-14)
changeset 24260d68040094415
parent 24259 c9e05c49d02c
child 24261 dd31811bdf46
PrimitiveDefs.dest_def;
Syntax.standard_read;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Tue Aug 14 13:20:17 2007 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Aug 14 13:20:18 2007 +0200
     1.3 @@ -484,7 +484,7 @@
     1.4    let val ((lhs, rhs), _) = tm
     1.5      |> no_vars pp
     1.6      |> Logic.strip_imp_concl
     1.7 -    |> Logic.dest_def pp Term.is_Const (K false) (K false)
     1.8 +    |> PrimitiveDefs.dest_def pp Term.is_Const (K false) (K false)
     1.9    in (Term.dest_Const (Term.head_of lhs), rhs) end
    1.10    handle TERM (msg, _) => error msg;
    1.11  
    1.12 @@ -500,7 +500,7 @@
    1.13  fun read_sort' syn ctxt str =
    1.14    let
    1.15      val thy = ProofContext.theory_of ctxt;
    1.16 -    val S = Syntax.read_sort ctxt syn (intern_sort thy) str;
    1.17 +    val S = Syntax.standard_read_sort ctxt syn (intern_sort thy) str;
    1.18    in certify_sort thy S handle TYPE (msg, _, _) => error msg end;
    1.19  
    1.20  fun read_sort thy str = read_sort' (syn_of thy) (ProofContext.init thy) str;
    1.21 @@ -546,7 +546,7 @@
    1.22    let
    1.23      val thy = ProofContext.theory_of ctxt;
    1.24      val T = intern_tycons thy
    1.25 -      (Syntax.read_typ ctxt syn (get_sort thy def_sort) (intern_sort thy) str);
    1.26 +      (Syntax.standard_read_typ ctxt syn (get_sort thy def_sort) (intern_sort thy) str);
    1.27    in cert thy T handle TYPE (msg, _, _) => error msg end
    1.28    handle ERROR msg => cat_error msg ("The error(s) above occurred in type " ^ quote str);
    1.29  
    1.30 @@ -626,7 +626,7 @@
    1.31            
    1.32      (*read term*)
    1.33      val map_const = try (#1 o Term.dest_Const o Consts.read_const consts);
    1.34 -    fun read T = disambig T o Syntax.read_term (get_sort thy def_sort) map_const map_free
    1.35 +    fun read T = disambig T o Syntax.standard_read_term (get_sort thy def_sort) map_const map_free
    1.36          (intern_tycons thy) (intern_sort thy) ctxt is_logtype syn T;
    1.37    in
    1.38      raw_args