# HG changeset patch
# User wenzelm
# Date 1427649847 -7200
# Node ID 2551ac44150ece123e91e597b6c4944080984b21
# Parent  0ab8750c9342af6f45304f0964f7c008ba4d95c3
tuned signature;

diff -r 0ab8750c9342 -r 2551ac44150e src/Pure/Syntax/local_syntax.ML
--- a/src/Pure/Syntax/local_syntax.ML	Sun Mar 29 19:23:08 2015 +0200
+++ b/src/Pure/Syntax/local_syntax.ML	Sun Mar 29 19:24:07 2015 +0200
@@ -55,7 +55,7 @@
     val thy_syntax = Sign.syn_of thy;
     fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
       | update_gram ((false, add, m), decls) =
-          Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
+          Syntax.update_const_gram add (Sign.logical_types thy) m decls;
 
     val local_syntax = thy_syntax
       |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
diff -r 0ab8750c9342 -r 2551ac44150e src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Sun Mar 29 19:23:08 2015 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Sun Mar 29 19:24:07 2015 +0200
@@ -26,7 +26,7 @@
   val make_type: int -> typ
   val binder_name: string -> string
   val syn_ext_types: (string * typ * mixfix) list -> Syntax_Ext.syn_ext
-  val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> Syntax_Ext.syn_ext
+  val syn_ext_consts: string list -> (string * typ * mixfix) list -> Syntax_Ext.syn_ext
 end;
 
 structure Mixfix: MIXFIX =
@@ -119,7 +119,7 @@
 val binder_stamp = stamp ();
 val binder_name = suffix "_binder";
 
-fun syn_ext_consts is_logtype const_decls =
+fun syn_ext_consts logical_types const_decls =
   let
     fun mk_infix sy ty c p1 p2 p3 =
       [Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], 1000),
@@ -152,7 +152,7 @@
 
     val consts = binders @ map (fn (c, _, _) => (c, "")) const_decls;
   in
-    Syntax_Ext.syn_ext' is_logtype mfix consts ([], binder_trs, binder_trs', []) ([], [])
+    Syntax_Ext.syn_ext' logical_types mfix consts ([], binder_trs, binder_trs', []) ([], [])
   end;
 
 end;
diff -r 0ab8750c9342 -r 2551ac44150e src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Mar 29 19:23:08 2015 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Mar 29 19:24:07 2015 +0200
@@ -108,7 +108,7 @@
     (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax
   val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
-  val update_const_gram: bool -> (string -> bool) ->
+  val update_const_gram: bool -> string list ->
     mode -> (string * typ * mixfix) list -> syntax -> syntax
   val update_trrules: Ast.ast trrule list -> syntax -> syntax
   val remove_trrules: Ast.ast trrule list -> syntax -> syntax
@@ -659,8 +659,8 @@
 fun update_type_gram add prmode decls =
   (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
 
-fun update_const_gram add is_logtype prmode decls =
-  (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
+fun update_const_gram add logical_types prmode decls =
+  (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts logical_types decls);
 
 val update_trrules = update_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
 val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
diff -r 0ab8750c9342 -r 2551ac44150e src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Sun Mar 29 19:23:08 2015 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Sun Mar 29 19:24:07 2015 +0200
@@ -31,7 +31,7 @@
   val mfix_delims: string -> string list
   val mfix_args: string -> int
   val escape: string -> string
-  val syn_ext': (string -> bool) -> mfix list ->
+  val syn_ext': string list -> mfix list ->
     (string * string) list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((Proof.context -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
@@ -184,8 +184,10 @@
 
 (* mfix_to_xprod *)
 
-fun mfix_to_xprod is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) =
+fun mfix_to_xprod logical_types (mfix as Mfix (sy, typ, const, pris, pri)) =
   let
+    val is_logtype = member (op =) logical_types;
+
     fun check_pri p =
       if p >= 0 andalso p <= 1000 then ()
       else err_in_mfix ("Precedence out of range: " ^ string_of_int p) mfix;
@@ -288,12 +290,12 @@
 
 (* syn_ext *)
 
-fun syn_ext' is_logtype mfixes consts trfuns (parse_rules, print_rules) =
+fun syn_ext' logical_types mfixes consts trfuns (parse_rules, print_rules) =
   let
     val (parse_ast_translation, parse_translation, print_translation,
       print_ast_translation) = trfuns;
 
-    val xprod_results = map (mfix_to_xprod is_logtype) mfixes;
+    val xprod_results = map (mfix_to_xprod logical_types) mfixes;
     val xprods = map #1 xprod_results;
     val consts' = map_filter #2 xprod_results;
     val parse_rules' = rev (map_filter #3 xprod_results);
@@ -311,7 +313,7 @@
   end;
 
 
-val syn_ext = syn_ext' (K false);
+val syn_ext = syn_ext' [];
 
 fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules;
 fun syn_ext_trfuns trfuns = syn_ext [] [] trfuns ([], []);
diff -r 0ab8750c9342 -r 2551ac44150e src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sun Mar 29 19:23:08 2015 +0200
+++ b/src/Pure/sign.ML	Sun Mar 29 19:24:07 2015 +0200
@@ -24,7 +24,7 @@
   val of_sort: theory -> typ * sort -> bool
   val inter_sort: theory -> sort * sort -> sort
   val witness_sorts: theory -> (typ * sort) list -> sort list -> (typ * sort) list
-  val is_logtype: theory -> string -> bool
+  val logical_types: theory -> string list
   val typ_instance: theory -> typ * typ -> bool
   val typ_equiv: theory -> typ * typ -> bool
   val typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv
@@ -190,7 +190,7 @@
 val of_sort = Type.of_sort o tsig_of;
 val inter_sort = Type.inter_sort o tsig_of;
 val witness_sorts = Type.witness_sorts o tsig_of;
-val is_logtype = member (op =) o Type.logical_types o tsig_of;
+val logical_types = Type.logical_types o tsig_of;
 
 val typ_instance = Type.typ_instance o tsig_of;
 fun typ_equiv thy (T, U) = typ_instance thy (T, U) andalso typ_instance thy (U, T);
@@ -369,7 +369,7 @@
     val ctxt = Type.set_mode Type.mode_syntax (Proof_Context.init_global thy);
     fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
       handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
-  in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
+  in thy |> map_syn (change_gram (logical_types thy) mode (map prep args)) end;
 
 fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x;
 
diff -r 0ab8750c9342 -r 2551ac44150e src/Pure/type.ML
--- a/src/Pure/type.ML	Sun Mar 29 19:23:08 2015 +0200
+++ b/src/Pure/type.ML	Sun Mar 29 19:24:07 2015 +0200
@@ -49,7 +49,6 @@
   val restore_mode: Proof.context -> Proof.context -> Proof.context
   val type_space: tsig -> Name_Space.T
   val type_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
-  val is_logtype: tsig -> string -> bool
   val check_decl: Context.generic -> tsig ->
     xstring * Position.T -> (string * Position.report list) * decl
   val the_decl: tsig -> string * Position.T -> decl
@@ -252,8 +251,6 @@
 fun type_alias naming binding name = map_tsig (fn (classes, default, types) =>
   (classes, default, (Name_Space.alias_table naming binding name types)));
 
-val is_logtype = member (op =) o logical_types;
-
 
 fun undecl_type c = "Undeclared type constructor: " ^ quote c;