src/Pure/sign.ML
changeset 59841 2551ac44150e
parent 56240 938c6c7e10eb
child 59880 30687c3f2b10
     1.1 --- a/src/Pure/sign.ML	Sun Mar 29 19:23:08 2015 +0200
     1.2 +++ b/src/Pure/sign.ML	Sun Mar 29 19:24:07 2015 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4    val of_sort: theory -> typ * sort -> bool
     1.5    val inter_sort: theory -> sort * sort -> sort
     1.6    val witness_sorts: theory -> (typ * sort) list -> sort list -> (typ * sort) list
     1.7 -  val is_logtype: theory -> string -> bool
     1.8 +  val logical_types: theory -> string list
     1.9    val typ_instance: theory -> typ * typ -> bool
    1.10    val typ_equiv: theory -> typ * typ -> bool
    1.11    val typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv
    1.12 @@ -190,7 +190,7 @@
    1.13  val of_sort = Type.of_sort o tsig_of;
    1.14  val inter_sort = Type.inter_sort o tsig_of;
    1.15  val witness_sorts = Type.witness_sorts o tsig_of;
    1.16 -val is_logtype = member (op =) o Type.logical_types o tsig_of;
    1.17 +val logical_types = Type.logical_types o tsig_of;
    1.18  
    1.19  val typ_instance = Type.typ_instance o tsig_of;
    1.20  fun typ_equiv thy (T, U) = typ_instance thy (T, U) andalso typ_instance thy (U, T);
    1.21 @@ -369,7 +369,7 @@
    1.22      val ctxt = Type.set_mode Type.mode_syntax (Proof_Context.init_global thy);
    1.23      fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
    1.24        handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
    1.25 -  in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
    1.26 +  in thy |> map_syn (change_gram (logical_types thy) mode (map prep args)) end;
    1.27  
    1.28  fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x;
    1.29