# HG changeset patch
# User wenzelm
# Date 1302091720 -7200
# Node ID 04bffad68aa4e67ca92d0b417789a2654b018861
# Parent  12fe41a92cd56e30eeac33ce0745eb15d8a300e1
discontinued old-style Syntax.constrainC;

diff -r 12fe41a92cd5 -r 04bffad68aa4 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Wed Apr 06 13:33:46 2011 +0200
+++ b/src/HOL/Groups.thy	Wed Apr 06 14:08:40 2011 +0200
@@ -130,7 +130,9 @@
       if not (null ts) orelse T = dummyT
         orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
       then raise Match
-      else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax_Phases.term_of_typ ctxt T);
+      else
+        Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $
+          Syntax_Phases.term_of_typ ctxt T);
   in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
 *} -- {* show types that are presumably too general *}
 
diff -r 12fe41a92cd5 -r 04bffad68aa4 src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Wed Apr 06 13:33:46 2011 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML	Wed Apr 06 14:08:40 2011 +0200
@@ -73,7 +73,7 @@
       let val t' =
         if not (Config.get ctxt show_types) andalso can Term.dest_Type T then syntax_numeral t
         else
-          Syntax.const Syntax.constrainC $ syntax_numeral t $
+          Syntax.const @{syntax_const "_constrain"} $ syntax_numeral t $
             Syntax_Phases.term_of_typ ctxt T
       in list_comb (t', ts) end
   | numeral_tr' _ T (t :: ts) =
diff -r 12fe41a92cd5 -r 04bffad68aa4 src/HOL/Tools/string_syntax.ML
--- a/src/HOL/Tools/string_syntax.ML	Wed Apr 06 13:33:46 2011 +0200
+++ b/src/HOL/Tools/string_syntax.ML	Wed Apr 06 14:08:40 2011 +0200
@@ -68,7 +68,7 @@
       (case Syntax.explode_xstr xstr of
         [] =>
           Ast.Appl
-            [Ast.Constant Syntax.constrainC,
+            [Ast.Constant @{syntax_const "_constrain"},
               Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}]
       | cs => mk_string cs)
   | string_ast_tr asts = raise Ast.AST ("string_tr", asts);
diff -r 12fe41a92cd5 -r 04bffad68aa4 src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Wed Apr 06 13:33:46 2011 +0200
+++ b/src/HOL/ex/Numeral.thy	Wed Apr 06 14:08:40 2011 +0200
@@ -309,7 +309,7 @@
       case T of
         Type (@{type_name fun}, [_, T']) =>
           if not (Config.get ctxt show_types) andalso can Term.dest_Type T' then t'
-          else Syntax.const Syntax.constrainC $ t' $ Syntax_Phases.term_of_typ ctxt T'
+          else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
       | T' => if T' = dummyT then t' else raise Match
     end;
 in [(@{const_syntax of_num}, num_tr')] end
diff -r 12fe41a92cd5 -r 04bffad68aa4 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Wed Apr 06 13:33:46 2011 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Wed Apr 06 14:08:40 2011 +0200
@@ -7,7 +7,6 @@
 signature SYN_EXT0 =
 sig
   val dddot_indexname: indexname
-  val constrainC: string
   val typeT: typ
   val spropT: typ
   val default_root: string Config.T
@@ -93,7 +92,6 @@
 (** misc definitions **)
 
 val dddot_indexname = ("dddot", 0);
-val constrainC = "_constrain";
 
 
 (* syntactic categories *)
diff -r 12fe41a92cd5 -r 04bffad68aa4 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 13:33:46 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 14:08:40 2011 +0200
@@ -545,7 +545,7 @@
 
     and constrain t T =
       if show_types andalso T <> dummyT then
-        Ast.Appl [Ast.Constant Syntax.constrainC, simple_ast_of ctxt t,
+        Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
           ast_of_termT ctxt trf (term_of_typ ctxt T)]
       else simple_ast_of ctxt t;
   in
@@ -639,7 +639,7 @@
 (* type constraints *)
 
 fun type_constraint_tr' ctxt (Type ("fun", [T, _])) (t :: ts) =
-      Term.list_comb (Lexicon.const Syntax.constrainC $ t $ term_of_typ ctxt T, ts)
+      Term.list_comb (Lexicon.const "_constrain" $ t $ term_of_typ ctxt T, ts)
   | type_constraint_tr' _ _ _ = raise Match;