discontinued old-style Syntax.constrainC;
authorwenzelm
Wed Apr 06 14:08:40 2011 +0200 (2011-04-06)
changeset 4224804bffad68aa4
parent 42247 12fe41a92cd5
child 42249 12a073670584
discontinued old-style Syntax.constrainC;
src/HOL/Groups.thy
src/HOL/Tools/numeral_syntax.ML
src/HOL/Tools/string_syntax.ML
src/HOL/ex/Numeral.thy
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syntax_phases.ML
     1.1 --- a/src/HOL/Groups.thy	Wed Apr 06 13:33:46 2011 +0200
     1.2 +++ b/src/HOL/Groups.thy	Wed Apr 06 14:08:40 2011 +0200
     1.3 @@ -130,7 +130,9 @@
     1.4        if not (null ts) orelse T = dummyT
     1.5          orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
     1.6        then raise Match
     1.7 -      else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax_Phases.term_of_typ ctxt T);
     1.8 +      else
     1.9 +        Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $
    1.10 +          Syntax_Phases.term_of_typ ctxt T);
    1.11    in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
    1.12  *} -- {* show types that are presumably too general *}
    1.13  
     2.1 --- a/src/HOL/Tools/numeral_syntax.ML	Wed Apr 06 13:33:46 2011 +0200
     2.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Wed Apr 06 14:08:40 2011 +0200
     2.3 @@ -73,7 +73,7 @@
     2.4        let val t' =
     2.5          if not (Config.get ctxt show_types) andalso can Term.dest_Type T then syntax_numeral t
     2.6          else
     2.7 -          Syntax.const Syntax.constrainC $ syntax_numeral t $
     2.8 +          Syntax.const @{syntax_const "_constrain"} $ syntax_numeral t $
     2.9              Syntax_Phases.term_of_typ ctxt T
    2.10        in list_comb (t', ts) end
    2.11    | numeral_tr' _ T (t :: ts) =
     3.1 --- a/src/HOL/Tools/string_syntax.ML	Wed Apr 06 13:33:46 2011 +0200
     3.2 +++ b/src/HOL/Tools/string_syntax.ML	Wed Apr 06 14:08:40 2011 +0200
     3.3 @@ -68,7 +68,7 @@
     3.4        (case Syntax.explode_xstr xstr of
     3.5          [] =>
     3.6            Ast.Appl
     3.7 -            [Ast.Constant Syntax.constrainC,
     3.8 +            [Ast.Constant @{syntax_const "_constrain"},
     3.9                Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}]
    3.10        | cs => mk_string cs)
    3.11    | string_ast_tr asts = raise Ast.AST ("string_tr", asts);
     4.1 --- a/src/HOL/ex/Numeral.thy	Wed Apr 06 13:33:46 2011 +0200
     4.2 +++ b/src/HOL/ex/Numeral.thy	Wed Apr 06 14:08:40 2011 +0200
     4.3 @@ -309,7 +309,7 @@
     4.4        case T of
     4.5          Type (@{type_name fun}, [_, T']) =>
     4.6            if not (Config.get ctxt show_types) andalso can Term.dest_Type T' then t'
     4.7 -          else Syntax.const Syntax.constrainC $ t' $ Syntax_Phases.term_of_typ ctxt T'
     4.8 +          else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
     4.9        | T' => if T' = dummyT then t' else raise Match
    4.10      end;
    4.11  in [(@{const_syntax of_num}, num_tr')] end
     5.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Apr 06 13:33:46 2011 +0200
     5.2 +++ b/src/Pure/Syntax/syn_ext.ML	Wed Apr 06 14:08:40 2011 +0200
     5.3 @@ -7,7 +7,6 @@
     5.4  signature SYN_EXT0 =
     5.5  sig
     5.6    val dddot_indexname: indexname
     5.7 -  val constrainC: string
     5.8    val typeT: typ
     5.9    val spropT: typ
    5.10    val default_root: string Config.T
    5.11 @@ -93,7 +92,6 @@
    5.12  (** misc definitions **)
    5.13  
    5.14  val dddot_indexname = ("dddot", 0);
    5.15 -val constrainC = "_constrain";
    5.16  
    5.17  
    5.18  (* syntactic categories *)
     6.1 --- a/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 13:33:46 2011 +0200
     6.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 14:08:40 2011 +0200
     6.3 @@ -545,7 +545,7 @@
     6.4  
     6.5      and constrain t T =
     6.6        if show_types andalso T <> dummyT then
     6.7 -        Ast.Appl [Ast.Constant Syntax.constrainC, simple_ast_of ctxt t,
     6.8 +        Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
     6.9            ast_of_termT ctxt trf (term_of_typ ctxt T)]
    6.10        else simple_ast_of ctxt t;
    6.11    in
    6.12 @@ -639,7 +639,7 @@
    6.13  (* type constraints *)
    6.14  
    6.15  fun type_constraint_tr' ctxt (Type ("fun", [T, _])) (t :: ts) =
    6.16 -      Term.list_comb (Lexicon.const Syntax.constrainC $ t $ term_of_typ ctxt T, ts)
    6.17 +      Term.list_comb (Lexicon.const "_constrain" $ t $ term_of_typ ctxt T, ts)
    6.18    | type_constraint_tr' _ _ _ = raise Match;
    6.19  
    6.20