# HG changeset patch
# User wenzelm
# Date 1147821826 -7200
# Node ID 853f5a3cc06e5828a87db993400d1988638bddff
# Parent  9be07d53169495097bc20de1b76aca745b179d14
always preserve authentic consts -- removed Syntax.mixfix_const;

diff -r 9be07d531694 -r 853f5a3cc06e src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed May 17 01:23:44 2006 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed May 17 01:23:46 2006 +0200
@@ -1124,7 +1124,7 @@
 fun add_abbrevs prmode = fold (fn (raw_c, raw_t, raw_mx) => fn ctxt =>
   let
     val ([(c, _, mx)], _) = cert_vars [(raw_c, NONE, raw_mx)] ctxt;
-    val (c', b) = Syntax.mixfix_const (full_name ctxt c) mx;
+    val c' = Syntax.constN ^ full_name ctxt c;
     val [t] = polymorphic ctxt [cert_term (ctxt |> expand_abbrevs false) raw_t];
     val T = Term.fastype_of t;
     val _ =
@@ -1133,8 +1133,8 @@
   in
     ctxt
     |> declare_term t
-    |> map_consts
-      (apsnd (Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) (#1 prmode) ((c, t), b)))
+    |> map_consts (apsnd
+      (Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) (#1 prmode) ((c, t), false)))
     |> map_syntax (LocalSyntax.add_modesyntax (theory_of ctxt) prmode [(false, (c', T, mx))])
   end);
 
diff -r 9be07d531694 -r 853f5a3cc06e src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Wed May 17 01:23:44 2006 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Wed May 17 01:23:46 2006 +0200
@@ -30,7 +30,6 @@
   val type_name: string -> mixfix -> string
   val const_name: string -> mixfix -> string
   val const_mixfix: string -> mixfix -> string * mixfix
-  val mixfix_const: string -> mixfix -> string * bool
   val unlocalize_mixfix: mixfix -> mixfix
   val mixfix_args: mixfix -> int
   val mixfix_content: mixfix -> string list list
@@ -130,9 +129,6 @@
 
 fun const_mixfix c mx = (const_name c mx, fix_mixfix c mx);
 
-fun mixfix_const c NoSyn = (c, true)
-  | mixfix_const c _ = (Lexicon.constN ^ c, false);
-
 fun map_mixfix _ NoSyn = NoSyn
   | map_mixfix f (Mixfix (sy, ps, p)) = Mixfix (f sy, ps, p)
   | map_mixfix f (Delimfix sy) = Delimfix (f sy)
diff -r 9be07d531694 -r 853f5a3cc06e src/Pure/consts.ML
--- a/src/Pure/consts.ML	Wed May 17 01:23:44 2006 +0200
+++ b/src/Pure/consts.ML	Wed May 17 01:23:46 2006 +0200
@@ -120,7 +120,7 @@
 fun syntax consts (c, mx) =
   let
     val ((T, _), early) = the_const consts c handle TYPE (msg, _, _) => error msg;
-    val c' = if early then NameSpace.base c else #1 (Syntax.mixfix_const c mx);
+    val c' = if early then NameSpace.base c else Syntax.constN ^ c;
   in (c', T, mx) end;
 
 
diff -r 9be07d531694 -r 853f5a3cc06e src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed May 17 01:23:44 2006 +0200
+++ b/src/Pure/sign.ML	Wed May 17 01:23:46 2006 +0200
@@ -725,7 +725,7 @@
     fun prep (raw_c, raw_T, raw_mx) =
       let
         val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
-        val (c', b) = if early then (c, true) else Syntax.mixfix_const (full_name thy c) mx;
+        val (c', b) = if early then (c, true) else (Syntax.constN ^ full_name thy c, false);
         val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
           cat_error msg ("in declaration of constant " ^ quote c);
       in (((c, T), b), (c', T, mx)) end;
@@ -754,13 +754,13 @@
       Term.no_dummy_patterns o cert_term_abbrev thy;
 
     val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
-    val (c', b) = Syntax.mixfix_const (full_name thy c) mx;
+    val c' = Syntax.constN ^ full_name thy c;
     val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg)
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
     val T = Term.fastype_of t;
   in
     thy
-    |> map_consts (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode ((c, t), b))
+    |> map_consts (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode ((c, t), false))
     |> map_syn (Syntax.extend_consts [c])
     |> add_modesyntax_i (mode, inout) [(c', T, mx)]
   end);