# HG changeset patch
# User wenzelm
# Date 1302265257 -7200
# Node ID d98eb048a2e4188f2974080f39c5ee14ae941e2e
# Parent  24075ad39ca24fc92b0ee3d9df0e72ac4192f1f5
discontinued special treatment of structure Mixfix;
eliminated slightly odd no_syn convenience;

diff -r 24075ad39ca2 -r d98eb048a2e4 src/HOL/HOLCF/Tools/cont_consts.ML
--- a/src/HOL/HOLCF/Tools/cont_consts.ML	Fri Apr 08 14:05:31 2011 +0200
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML	Fri Apr 08 14:20:57 2011 +0200
@@ -50,7 +50,7 @@
     fun syntax b = Syntax.mark_const (Sign.full_bname thy b)
     val c1 = Binding.name_of c
     val c2 = c1 ^ "_cont_syntax"
-    val n = Syntax.mixfix_args mx
+    val n = Mixfix.mixfix_args mx
   in
     ((c, T, NoSyn),
       (Binding.name c2, change_arrow n T, mx),
@@ -64,7 +64,7 @@
   | is_contconst (_, _, Binder _) = false    (* FIXME ? *)
   | is_contconst (c, T, mx) =
       let
-        val n = Syntax.mixfix_args mx handle ERROR msg =>
+        val n = Mixfix.mixfix_args mx handle ERROR msg =>
           cat_error msg ("in mixfix annotation for " ^ quote (Binding.str_of c))
       in cfun_arity T >= n end
 
diff -r 24075ad39ca2 -r d98eb048a2e4 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Fri Apr 08 14:05:31 2011 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Fri Apr 08 14:20:57 2011 +0200
@@ -178,7 +178,7 @@
 
 (* Compatibility. *)
 
-val string_of_mixfix = Pretty.string_of o Syntax.pretty_mixfix;
+val string_of_mixfix = Pretty.string_of o Mixfix.pretty_mixfix;
 
 fun mk_syn thy c =
   if Syntax.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn
diff -r 24075ad39ca2 -r d98eb048a2e4 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Apr 08 14:05:31 2011 +0200
+++ b/src/HOL/Orderings.thy	Fri Apr 08 14:20:57 2011 +0200
@@ -638,8 +638,8 @@
 
 print_translation {*
 let
-  val All_binder = Syntax.binder_name @{const_syntax All};
-  val Ex_binder = Syntax.binder_name @{const_syntax Ex};
+  val All_binder = Mixfix.binder_name @{const_syntax All};
+  val Ex_binder = Mixfix.binder_name @{const_syntax Ex};
   val impl = @{const_syntax HOL.implies};
   val conj = @{const_syntax HOL.conj};
   val less = @{const_syntax less};
diff -r 24075ad39ca2 -r d98eb048a2e4 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Apr 08 14:05:31 2011 +0200
+++ b/src/HOL/Set.thy	Fri Apr 08 14:20:57 2011 +0200
@@ -231,8 +231,8 @@
 print_translation {*
 let
   val Type (set_type, _) = @{typ "'a set"};   (* FIXME 'a => bool (!?!) *)
-  val All_binder = Syntax.binder_name @{const_syntax All};
-  val Ex_binder = Syntax.binder_name @{const_syntax Ex};
+  val All_binder = Mixfix.binder_name @{const_syntax All};
+  val Ex_binder = Mixfix.binder_name @{const_syntax Ex};
   val impl = @{const_syntax HOL.implies};
   val conj = @{const_syntax HOL.conj};
   val sbset = @{const_syntax subset};
diff -r 24075ad39ca2 -r d98eb048a2e4 src/HOL/Statespace/DistinctTreeProver.thy
--- a/src/HOL/Statespace/DistinctTreeProver.thy	Fri Apr 08 14:05:31 2011 +0200
+++ b/src/HOL/Statespace/DistinctTreeProver.thy	Fri Apr 08 14:20:57 2011 +0200
@@ -643,8 +643,7 @@
 *)
 val nums = (0 upto 10000);
 val nums' = (0 upto 3000);
-val const_decls = map (fn i => Syntax.no_syn 
-                                 ("const" ^ string_of_int i,Type ("nat",[]))) nums
+val const_decls = map (fn i => ("const" ^ string_of_int i, Type ("nat", []), NoSyn)) nums
 
 val consts = sort Term_Ord.fast_term_ord 
               (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)
diff -r 24075ad39ca2 -r d98eb048a2e4 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Fri Apr 08 14:05:31 2011 +0200
+++ b/src/HOL/Statespace/state_space.ML	Fri Apr 08 14:20:57 2011 +0200
@@ -344,8 +344,6 @@
 
 fun K_const T = Const ("StateFun.K_statefun",T --> T --> T);
 
-val no_syn = #3 (Syntax.no_syn ((),()));
-
 
 fun add_declaration name decl thy =
   thy
diff -r 24075ad39ca2 -r d98eb048a2e4 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Fri Apr 08 14:05:31 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Fri Apr 08 14:20:57 2011 +0200
@@ -47,10 +47,9 @@
       val eqs_t = mk_equations (map2 (fn name => fn T => Free (name, T)) names Ts)
     in
       Function.add_function
-        (map (fn (name, T) =>
-            Syntax.no_syn (Binding.conceal (Binding.name name), SOME T))
-              (names ~~ Ts))
-          (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs_t)
+        (map (fn (name, T) => (Binding.conceal (Binding.name name), SOME T, NoSyn))
+          (names ~~ Ts))
+        (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs_t)
         Function_Common.default_config pat_completeness_auto
       #> snd
       #> Local_Theory.restore
diff -r 24075ad39ca2 -r d98eb048a2e4 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Fri Apr 08 14:05:31 2011 +0200
+++ b/src/Pure/Isar/element.ML	Fri Apr 08 14:20:57 2011 +0200
@@ -169,7 +169,7 @@
     val prt_name_atts = pretty_name_atts ctxt;
 
     fun prt_mixfix NoSyn = []
-      | prt_mixfix mx = [Pretty.brk 2, Syntax.pretty_mixfix mx];
+      | prt_mixfix mx = [Pretty.brk 2, Mixfix.pretty_mixfix mx];
 
     fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Binding.name_of x ^ " ::") ::
           Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
diff -r 24075ad39ca2 -r d98eb048a2e4 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Fri Apr 08 14:05:31 2011 +0200
+++ b/src/Pure/Isar/generic_target.ML	Fri Apr 08 14:20:57 2011 +0200
@@ -42,7 +42,7 @@
       ("Additional type variable(s) in specification of " ^ Binding.str_of b ^ ": " ^
         commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
         (if mx = NoSyn then ""
-         else "\nDropping mixfix syntax " ^ Pretty.string_of (Syntax.pretty_mixfix mx)));
+         else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)));
       NoSyn);
 
 
diff -r 24075ad39ca2 -r d98eb048a2e4 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Fri Apr 08 14:05:31 2011 +0200
+++ b/src/Pure/Isar/parse.ML	Fri Apr 08 14:20:57 2011 +0200
@@ -305,7 +305,7 @@
 
 val fixes =
   and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) ||
-    params >> map Syntax.no_syn) >> flat;
+    params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
 
 val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];
 val for_simple_fixes = Scan.optional ($$$ "for" |-- !!! simple_fixes) [];
diff -r 24075ad39ca2 -r d98eb048a2e4 src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Fri Apr 08 14:05:31 2011 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Fri Apr 08 14:20:57 2011 +0200
@@ -87,7 +87,7 @@
 val locale_fixes =
   Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix
     >> (single o Parse.triple1) ||
-  Parse.params >> map Syntax.no_syn) >> flat;
+  Parse.params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
 
 val locale_insts =
   Scan.optional
diff -r 24075ad39ca2 -r d98eb048a2e4 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Apr 08 14:05:31 2011 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Apr 08 14:20:57 2011 +0200
@@ -566,7 +566,7 @@
 
 val write_cmd =
   gen_write (fn ctxt => fn (c, mx) =>
-    (ProofContext.read_const ctxt false (Syntax.mixfixT mx) c, mx));
+    (ProofContext.read_const ctxt false (Mixfix.mixfixT mx) c, mx));
 
 end;
 
diff -r 24075ad39ca2 -r d98eb048a2e4 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Apr 08 14:05:31 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Apr 08 14:20:57 2011 +0200
@@ -915,7 +915,7 @@
 (* variables *)
 
 fun declare_var (x, opt_T, mx) ctxt =
-  let val T = (case opt_T of SOME T => T | NONE => Syntax.mixfixT mx)
+  let val T = (case opt_T of SOME T => T | NONE => Mixfix.mixfixT mx)
   in ((x, T, mx), ctxt |> Variable.declare_constraints (Free (x, T))) end;
 
 local
@@ -978,7 +978,7 @@
 local
 
 fun type_syntax (Type (c, args), mx) =
-      SOME (Local_Syntax.Type, (Syntax.mark_type c, Syntax.make_type (length args), mx))
+      SOME (Local_Syntax.Type, (Syntax.mark_type c, Mixfix.make_type (length args), mx))
   | type_syntax _ = NONE;
 
 fun const_syntax _ (Free (x, T), mx) = SOME (Local_Syntax.Fixed, (x, T, mx))
diff -r 24075ad39ca2 -r d98eb048a2e4 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Fri Apr 08 14:05:31 2011 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Fri Apr 08 14:20:57 2011 +0200
@@ -4,7 +4,7 @@
 Mixfix declarations, infixes, binders.
 *)
 
-signature MIXFIX0 =
+signature BASIC_MIXFIX =
 sig
   datatype mixfix =
     NoSyn |
@@ -15,22 +15,16 @@
     Infixr of string * int |
     Binder of string * int * int |
     Structure
-  val binder_name: string -> string
 end;
 
-signature MIXFIX1 =
+signature MIXFIX =
 sig
-  include MIXFIX0
-  val no_syn: 'a * 'b -> 'a * 'b * mixfix
+  include BASIC_MIXFIX
   val pretty_mixfix: mixfix -> Pretty.T
   val mixfix_args: mixfix -> int
   val mixfixT: mixfix -> typ
   val make_type: int -> typ
-end;
-
-signature MIXFIX =
-sig
-  include MIXFIX1
+  val binder_name: string -> string
   val syn_ext_types: (string * typ * mixfix) list -> Syn_Ext.syn_ext
   val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> Syn_Ext.syn_ext
 end;
@@ -38,7 +32,6 @@
 structure Mixfix: MIXFIX =
 struct
 
-
 (** mixfix declarations **)
 
 datatype mixfix =
@@ -51,8 +44,6 @@
   Binder of string * int * int |
   Structure;
 
-fun no_syn (x, y) = (x, y, NoSyn);
-
 
 (* pretty_mixfix *)
 
@@ -164,3 +155,7 @@
   end;
 
 end;
+
+structure Basic_Mixfix: BASIC_MIXFIX = Mixfix;
+open Basic_Mixfix;
+
diff -r 24075ad39ca2 -r d98eb048a2e4 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Apr 08 14:05:31 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Apr 08 14:20:57 2011 +0200
@@ -7,7 +7,6 @@
 
 signature BASIC_SYNTAX =
 sig
-  include MIXFIX0
   include PRINTER0
 end;
 
@@ -15,7 +14,6 @@
 sig
   include LEXICON0
   include SYN_EXT0
-  include MIXFIX1
   include PRINTER0
   val positions_raw: Config.raw
   val positions: bool Config.T
@@ -725,7 +723,7 @@
 
 (*export parts of internal Syntax structures*)
 val syntax_tokenize = tokenize;
-open Lexicon Syn_Ext Mixfix Printer;
+open Lexicon Syn_Ext Printer;
 val tokenize = syntax_tokenize;
 
 end;
@@ -734,5 +732,4 @@
 open Basic_Syntax;
 
 forget_structure "Syn_Ext";
-forget_structure "Mixfix";
 
diff -r 24075ad39ca2 -r d98eb048a2e4 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Apr 08 14:05:31 2011 +0200
+++ b/src/Pure/sign.ML	Fri Apr 08 14:20:57 2011 +0200
@@ -334,7 +334,7 @@
 fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   let
     fun type_syntax (b, n, mx) =
-      (Syntax.mark_type (Name_Space.full_name naming b), Syntax.make_type n, mx);
+      (Syntax.mark_type (Name_Space.full_name naming b), Mixfix.make_type n, mx);
     val syn' = Syntax.update_type_gram true Syntax.mode_default (map type_syntax types) syn;
     val tsig' = fold (fn (a, n, _) => Type.add_type naming (a, n)) types tsig;
   in (naming, syn', tsig', consts) end);
@@ -373,7 +373,7 @@
 fun type_notation add mode args =
   let
     fun type_syntax (Type (c, args), mx) =
-          SOME (Syntax.mark_type c, Syntax.make_type (length args), mx)
+          SOME (Syntax.mark_type c, Mixfix.make_type (length args), mx)
       | type_syntax _ = NONE;
   in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end;