tuned signature;
authorwenzelm
Wed Nov 09 20:47:11 2011 +0100 (2011-11-09)
changeset 45429fd58cbf8cae3
parent 45428 aa35c9454a95
child 45430 b8eb7a791dac
tuned signature;
tuned;
src/HOL/Tools/code_evaluation.ML
src/Pure/Isar/class.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/overloading.ML
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/type_infer_context.ML
src/Tools/adhoc_overloading.ML
src/Tools/subtyping.ML
     1.1 --- a/src/HOL/Tools/code_evaluation.ML	Wed Nov 09 19:01:50 2011 +0100
     1.2 +++ b/src/HOL/Tools/code_evaluation.ML	Wed Nov 09 20:47:11 2011 +0100
     1.3 @@ -224,7 +224,7 @@
     1.4    #> Code.abstype_interpretation ensure_term_of
     1.5    #> Code.datatype_interpretation ensure_term_of_code
     1.6    #> Code.abstype_interpretation ensure_abs_term_of_code
     1.7 -  #> Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
     1.8 +  #> Context.theory_map (Syntax_Phases.term_check 0 "termify" check_termify)
     1.9    #> Value.add_evaluator ("code", dynamic_value_strict o Proof_Context.theory_of);
    1.10  
    1.11  end;
     2.1 --- a/src/Pure/Isar/class.ML	Wed Nov 09 19:01:50 2011 +0100
     2.2 +++ b/src/Pure/Isar/class.ML	Wed Nov 09 20:47:11 2011 +0100
     2.3 @@ -550,7 +550,7 @@
     2.4      |> (Overloading.map_improvable_syntax o apfst)
     2.5           (K ((primary_constraints, []), (((improve, K NONE), false), [])))
     2.6      |> Overloading.activate_improvable_syntax
     2.7 -    |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check)
     2.8 +    |> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check)
     2.9      |> synchronize_inst_syntax
    2.10      |> Local_Theory.init NONE ""
    2.11         {define = Generic_Target.define foundation,
     3.1 --- a/src/Pure/Isar/class_declaration.ML	Wed Nov 09 19:01:50 2011 +0100
     3.2 +++ b/src/Pure/Isar/class_declaration.ML	Wed Nov 09 20:47:11 2011 +0100
     3.3 @@ -147,11 +147,11 @@
     3.4      val init_class_body =
     3.5        fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
     3.6        #> Class.redeclare_operations thy sups
     3.7 -      #> Context.proof_map (Syntax.add_typ_check 10 "reject_bcd_etc" (K reject_bcd_etc))
     3.8 -      #> Context.proof_map (Syntax.add_typ_check ~10 "singleton_fixate" (K singleton_fixate));
     3.9 +      #> Context.proof_map (Syntax_Phases.typ_check 10 "reject_bcd_etc" (K reject_bcd_etc))
    3.10 +      #> Context.proof_map (Syntax_Phases.typ_check ~10 "singleton_fixate" (K singleton_fixate));
    3.11      val ((raw_supparams, _, raw_inferred_elems), _) =
    3.12        Proof_Context.init_global thy
    3.13 -      |> Context.proof_map (Syntax.add_typ_check 5 "after_infer_fixate" (K after_infer_fixate))
    3.14 +      |> Context.proof_map (Syntax_Phases.typ_check 5 "after_infer_fixate" (K after_infer_fixate))
    3.15        |> prep_decl raw_supexpr init_class_body raw_elems;
    3.16      fun filter_element (Element.Fixes []) = NONE
    3.17        | filter_element (e as Element.Fixes _) = SOME e
     4.1 --- a/src/Pure/Isar/overloading.ML	Wed Nov 09 19:01:50 2011 +0100
     4.2 +++ b/src/Pure/Isar/overloading.ML	Wed Nov 09 20:47:11 2011 +0100
     4.3 @@ -114,8 +114,8 @@
     4.4  
     4.5  val activate_improvable_syntax =
     4.6    Context.proof_map
     4.7 -    (Syntax.context_term_check 0 "improvement" improve_term_check
     4.8 -    #> Syntax.context_term_uncheck 0 "improvement" improve_term_uncheck)
     4.9 +    (Syntax_Phases.context_term_check 0 "improvement" improve_term_check
    4.10 +    #> Syntax_Phases.context_term_uncheck 0 "improvement" improve_term_uncheck)
    4.11    #> set_primary_constraints;
    4.12  
    4.13  
     5.1 --- a/src/Pure/Isar/proof_context.ML	Wed Nov 09 19:01:50 2011 +0100
     5.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Nov 09 20:47:11 2011 +0100
     5.3 @@ -83,6 +83,9 @@
     5.4    val cert_term: Proof.context -> term -> term
     5.5    val cert_prop: Proof.context -> term -> term
     5.6    val def_type: Proof.context -> indexname -> typ option
     5.7 +  val standard_typ_check: Proof.context -> typ list -> typ list
     5.8 +  val standard_term_check_finish: Proof.context -> term list -> term list
     5.9 +  val standard_term_uncheck: Proof.context -> term list -> term list
    5.10    val goal_export: Proof.context -> Proof.context -> thm list -> thm list
    5.11    val export: Proof.context -> Proof.context -> thm list -> thm list
    5.12    val export_morphism: Proof.context -> Proof.context -> morphism
    5.13 @@ -666,23 +669,12 @@
    5.14    let val Mode {pattern, ...} = get_mode ctxt
    5.15    in Variable.def_type ctxt pattern end;
    5.16  
    5.17 -local
    5.18 -
    5.19  fun standard_typ_check ctxt =
    5.20 -  map (cert_typ_mode (Type.get_mode ctxt) ctxt) #>
    5.21 -  map (prepare_patternT ctxt);
    5.22 -
    5.23 -fun standard_term_uncheck ctxt =
    5.24 -  map (contract_abbrevs ctxt);
    5.25 +  map (cert_typ_mode (Type.get_mode ctxt) ctxt #> prepare_patternT ctxt);
    5.26  
    5.27 -in
    5.28 +val standard_term_check_finish = prepare_patterns;
    5.29  
    5.30 -val _ = Context.>>
    5.31 - (Syntax.add_typ_check 0 "standard" standard_typ_check #>
    5.32 -  Syntax.add_term_check 100 "fixate" prepare_patterns #>
    5.33 -  Syntax.add_term_uncheck 0 "standard" standard_term_uncheck);
    5.34 -
    5.35 -end;
    5.36 +fun standard_term_uncheck ctxt = map (contract_abbrevs ctxt);
    5.37  
    5.38  
    5.39  
     6.1 --- a/src/Pure/Syntax/syntax.ML	Wed Nov 09 19:01:50 2011 +0100
     6.2 +++ b/src/Pure/Syntax/syntax.ML	Wed Nov 09 20:47:11 2011 +0100
     6.3 @@ -30,31 +30,6 @@
     6.4    val unparse_arity: Proof.context -> arity -> Pretty.T
     6.5    val unparse_typ: Proof.context -> typ -> Pretty.T
     6.6    val unparse_term: Proof.context -> term -> Pretty.T
     6.7 -  val print_checks: Proof.context -> unit
     6.8 -  val context_typ_check: int -> string ->
     6.9 -    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
    6.10 -    Context.generic -> Context.generic
    6.11 -  val context_term_check: int -> string ->
    6.12 -    (term list -> Proof.context -> (term list * Proof.context) option) ->
    6.13 -    Context.generic -> Context.generic
    6.14 -  val context_typ_uncheck: int -> string ->
    6.15 -    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
    6.16 -    Context.generic -> Context.generic
    6.17 -  val context_term_uncheck: int -> string ->
    6.18 -    (term list -> Proof.context -> (term list * Proof.context) option) ->
    6.19 -    Context.generic -> Context.generic
    6.20 -  val add_typ_check: int -> string -> (Proof.context -> typ list -> typ list) ->
    6.21 -    Context.generic -> Context.generic
    6.22 -  val add_term_check: int -> string -> (Proof.context -> term list -> term list) ->
    6.23 -    Context.generic -> Context.generic
    6.24 -  val add_typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) ->
    6.25 -    Context.generic -> Context.generic
    6.26 -  val add_term_uncheck: int -> string -> (Proof.context -> term list -> term list) ->
    6.27 -    Context.generic -> Context.generic
    6.28 -  val apply_typ_check: Proof.context -> typ list -> typ list
    6.29 -  val apply_term_check: Proof.context -> term list -> term list
    6.30 -  val apply_typ_uncheck: Proof.context -> typ list -> typ list
    6.31 -  val apply_term_uncheck: Proof.context -> term list -> term list
    6.32    val check_sort: Proof.context -> sort -> sort
    6.33    val check_typ: Proof.context -> typ -> typ
    6.34    val check_term: Proof.context -> term -> term
    6.35 @@ -244,88 +219,7 @@
    6.36  val unparse_term = operation #unparse_term;
    6.37  
    6.38  
    6.39 -(* context-sensitive (un)checking *)
    6.40 -
    6.41 -type key = int * bool;
    6.42 -
    6.43 -structure Checks = Generic_Data
    6.44 -(
    6.45 -  type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
    6.46 -  type T =
    6.47 -    ((key * ((string * typ check) * stamp) list) list *
    6.48 -     (key * ((string * term check) * stamp) list) list);
    6.49 -  val empty = ([], []);
    6.50 -  val extend = I;
    6.51 -  fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
    6.52 -    (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
    6.53 -     AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
    6.54 -);
    6.55 -
    6.56 -fun print_checks ctxt =
    6.57 -  let
    6.58 -    fun split_checks checks =
    6.59 -      List.partition (fn ((_, un), _) => not un) checks
    6.60 -      |> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs))
    6.61 -          #> sort (int_ord o pairself fst));
    6.62 -    fun pretty_checks kind checks =
    6.63 -      checks |> map (fn (i, names) => Pretty.block
    6.64 -        [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"),
    6.65 -          Pretty.brk 1, Pretty.strs names]);
    6.66 -
    6.67 -    val (typs, terms) = Checks.get (Context.Proof ctxt);
    6.68 -    val (typ_checks, typ_unchecks) = split_checks typs;
    6.69 -    val (term_checks, term_unchecks) = split_checks terms;
    6.70 -  in
    6.71 -    pretty_checks "typ_checks" typ_checks @
    6.72 -    pretty_checks "term_checks" term_checks @
    6.73 -    pretty_checks "typ_unchecks" typ_unchecks @
    6.74 -    pretty_checks "term_unchecks" term_unchecks
    6.75 -  end |> Pretty.chunks |> Pretty.writeln;
    6.76 -
    6.77 -
    6.78 -local
    6.79 -
    6.80 -fun context_check which (key: key) name f =
    6.81 -  Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
    6.82 -
    6.83 -fun simple_check eq f xs ctxt =
    6.84 -  let val xs' = f ctxt xs
    6.85 -  in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end;
    6.86 -
    6.87 -in
    6.88 -
    6.89 -fun context_typ_check stage = context_check apfst (stage, false);
    6.90 -fun context_term_check stage = context_check apsnd (stage, false);
    6.91 -fun context_typ_uncheck stage = context_check apfst (stage, true);
    6.92 -fun context_term_uncheck stage = context_check apsnd (stage, true);
    6.93 -
    6.94 -fun add_typ_check key name f = context_typ_check key name (simple_check (op =) f);
    6.95 -fun add_term_check key name f = context_term_check key name (simple_check (op aconv) f);
    6.96 -fun add_typ_uncheck key name f = context_typ_uncheck key name (simple_check (op =) f);
    6.97 -fun add_term_uncheck key name f = context_term_uncheck key name (simple_check (op aconv) f);
    6.98 -
    6.99 -end;
   6.100 -
   6.101 -
   6.102 -local
   6.103 -
   6.104 -fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
   6.105 -fun check_all fs = perhaps_apply (map check_stage fs);
   6.106 -
   6.107 -fun check which uncheck ctxt0 xs0 =
   6.108 -  let
   6.109 -    val funs = which (Checks.get (Context.Proof ctxt0))
   6.110 -      |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
   6.111 -      |> Library.sort (int_ord o pairself fst) |> map snd
   6.112 -      |> not uncheck ? map rev;
   6.113 -  in #1 (perhaps (check_all funs) (xs0, ctxt0)) end;
   6.114 -
   6.115 -in
   6.116 -
   6.117 -val apply_typ_check = check fst false;
   6.118 -val apply_term_check = check snd false;
   6.119 -val apply_typ_uncheck = check fst true;
   6.120 -val apply_term_uncheck = check snd true;
   6.121 +(* (un)checking *)
   6.122  
   6.123  val check_typs = operation #check_typs;
   6.124  val check_terms = operation #check_terms;
   6.125 @@ -338,8 +232,6 @@
   6.126  val uncheck_typs = operation #uncheck_typs;
   6.127  val uncheck_terms = operation #uncheck_terms;
   6.128  
   6.129 -end;
   6.130 -
   6.131  
   6.132  (* derived operations for algebra of sorts *)
   6.133  
     7.1 --- a/src/Pure/Syntax/syntax_phases.ML	Wed Nov 09 19:01:50 2011 +0100
     7.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Wed Nov 09 20:47:11 2011 +0100
     7.3 @@ -13,6 +13,27 @@
     7.4      Position.report list * term Exn.result -> Position.report list * term Exn.result
     7.5    val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
     7.6    val term_of_typ: Proof.context -> typ -> term
     7.7 +  val print_checks: Proof.context -> unit
     7.8 +  val context_typ_check: int -> string ->
     7.9 +    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
    7.10 +    Context.generic -> Context.generic
    7.11 +  val context_term_check: int -> string ->
    7.12 +    (term list -> Proof.context -> (term list * Proof.context) option) ->
    7.13 +    Context.generic -> Context.generic
    7.14 +  val context_typ_uncheck: int -> string ->
    7.15 +    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
    7.16 +    Context.generic -> Context.generic
    7.17 +  val context_term_uncheck: int -> string ->
    7.18 +    (term list -> Proof.context -> (term list * Proof.context) option) ->
    7.19 +    Context.generic -> Context.generic
    7.20 +  val typ_check: int -> string -> (Proof.context -> typ list -> typ list) ->
    7.21 +    Context.generic -> Context.generic
    7.22 +  val term_check: int -> string -> (Proof.context -> term list -> term list) ->
    7.23 +    Context.generic -> Context.generic
    7.24 +  val typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) ->
    7.25 +    Context.generic -> Context.generic
    7.26 +  val term_uncheck: int -> string -> (Proof.context -> term list -> term list) ->
    7.27 +    Context.generic -> Context.generic
    7.28  end
    7.29  
    7.30  structure Syntax_Phases: SYNTAX_PHASES =
    7.31 @@ -692,6 +713,87 @@
    7.32  
    7.33  (** check/uncheck **)
    7.34  
    7.35 +(* context-sensitive (un)checking *)
    7.36 +
    7.37 +type key = int * bool;
    7.38 +
    7.39 +structure Checks = Generic_Data
    7.40 +(
    7.41 +  type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
    7.42 +  type T =
    7.43 +    ((key * ((string * typ check) * stamp) list) list *
    7.44 +     (key * ((string * term check) * stamp) list) list);
    7.45 +  val empty = ([], []);
    7.46 +  val extend = I;
    7.47 +  fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
    7.48 +    (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
    7.49 +     AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
    7.50 +);
    7.51 +
    7.52 +fun print_checks ctxt =
    7.53 +  let
    7.54 +    fun split_checks checks =
    7.55 +      List.partition (fn ((_, un), _) => not un) checks
    7.56 +      |> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs))
    7.57 +          #> sort (int_ord o pairself fst));
    7.58 +    fun pretty_checks kind checks =
    7.59 +      checks |> map (fn (i, names) => Pretty.block
    7.60 +        [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"),
    7.61 +          Pretty.brk 1, Pretty.strs names]);
    7.62 +
    7.63 +    val (typs, terms) = Checks.get (Context.Proof ctxt);
    7.64 +    val (typ_checks, typ_unchecks) = split_checks typs;
    7.65 +    val (term_checks, term_unchecks) = split_checks terms;
    7.66 +  in
    7.67 +    pretty_checks "typ_checks" typ_checks @
    7.68 +    pretty_checks "term_checks" term_checks @
    7.69 +    pretty_checks "typ_unchecks" typ_unchecks @
    7.70 +    pretty_checks "term_unchecks" term_unchecks
    7.71 +  end |> Pretty.chunks |> Pretty.writeln;
    7.72 +
    7.73 +
    7.74 +local
    7.75 +
    7.76 +fun context_check which (key: key) name f =
    7.77 +  Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
    7.78 +
    7.79 +fun simple_check eq f xs ctxt =
    7.80 +  let val xs' = f ctxt xs
    7.81 +  in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end;
    7.82 +
    7.83 +in
    7.84 +
    7.85 +fun context_typ_check stage = context_check apfst (stage, false);
    7.86 +fun context_term_check stage = context_check apsnd (stage, false);
    7.87 +fun context_typ_uncheck stage = context_check apfst (stage, true);
    7.88 +fun context_term_uncheck stage = context_check apsnd (stage, true);
    7.89 +
    7.90 +fun typ_check key name f = context_typ_check key name (simple_check (op =) f);
    7.91 +fun term_check key name f = context_term_check key name (simple_check (op aconv) f);
    7.92 +fun typ_uncheck key name f = context_typ_uncheck key name (simple_check (op =) f);
    7.93 +fun term_uncheck key name f = context_term_uncheck key name (simple_check (op aconv) f);
    7.94 +
    7.95 +end;
    7.96 +
    7.97 +
    7.98 +local
    7.99 +
   7.100 +fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
   7.101 +fun check_all fs = perhaps_apply (map check_stage fs);
   7.102 +
   7.103 +fun check which uncheck ctxt0 xs0 =
   7.104 +  let
   7.105 +    val funs = which (Checks.get (Context.Proof ctxt0))
   7.106 +      |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
   7.107 +      |> Library.sort (int_ord o pairself fst) |> map snd
   7.108 +      |> not uncheck ? map rev;
   7.109 +  in #1 (perhaps (check_all funs) (xs0, ctxt0)) end;
   7.110 +
   7.111 +val apply_typ_check = check fst false;
   7.112 +val apply_term_check = check snd false;
   7.113 +val apply_typ_uncheck = check fst true;
   7.114 +val apply_term_uncheck = check snd true;
   7.115 +
   7.116  fun prepare_types ctxt tys =
   7.117    let
   7.118      fun constraint (xi: indexname, S) = S <> dummyS ? insert (op =) (xi, S);
   7.119 @@ -708,20 +810,34 @@
   7.120          | T => T) tys
   7.121    end;
   7.122  
   7.123 +in
   7.124 +
   7.125  fun check_typs ctxt =
   7.126    prepare_types ctxt #>
   7.127 -  Syntax.apply_typ_check ctxt #>
   7.128 +  apply_typ_check ctxt #>
   7.129    Term_Sharing.typs (Proof_Context.theory_of ctxt);
   7.130  
   7.131  fun check_terms ctxt =
   7.132    Term.burrow_types (prepare_types ctxt) #>
   7.133 -  Syntax.apply_term_check ctxt #>
   7.134 +  apply_term_check ctxt #>
   7.135    Term_Sharing.terms (Proof_Context.theory_of ctxt);
   7.136  
   7.137  fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
   7.138  
   7.139 -val uncheck_typs = Syntax.apply_typ_uncheck;
   7.140 -val uncheck_terms = Syntax.apply_term_uncheck;
   7.141 +val uncheck_typs = apply_typ_uncheck;
   7.142 +val uncheck_terms = apply_term_uncheck;
   7.143 +
   7.144 +end;
   7.145 +
   7.146 +
   7.147 +(* standard phases *)
   7.148 +
   7.149 +val _ = Context.>>
   7.150 + (typ_check 0 "standard" Proof_Context.standard_typ_check #>
   7.151 +  term_check 0 "standard"
   7.152 +    (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #>
   7.153 +  term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #>
   7.154 +  term_uncheck 0 "standard" Proof_Context.standard_term_uncheck);
   7.155  
   7.156  
   7.157  
     8.1 --- a/src/Pure/type_infer_context.ML	Wed Nov 09 19:01:50 2011 +0100
     8.2 +++ b/src/Pure/type_infer_context.ML	Wed Nov 09 20:47:11 2011 +0100
     8.3 @@ -259,9 +259,4 @@
     8.4      val (_, ts') = Type_Infer.finish ctxt tye ([], ts);
     8.5    in ts' end;
     8.6  
     8.7 -val _ =
     8.8 -  Context.>>
     8.9 -    (Syntax.add_term_check 0 "standard"
    8.10 -      (fn ctxt => infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)));
    8.11 -
    8.12  end;
     9.1 --- a/src/Tools/adhoc_overloading.ML	Wed Nov 09 19:01:50 2011 +0100
     9.2 +++ b/src/Tools/adhoc_overloading.ML	Wed Nov 09 20:47:11 2011 +0100
     9.3 @@ -132,8 +132,8 @@
     9.4  (* setup *)
     9.5  
     9.6  val setup = Context.theory_map
     9.7 -  (Syntax.context_term_check 0 "adhoc_overloading" check
     9.8 -   #> Syntax.context_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
     9.9 -   #> Syntax.context_term_uncheck 0 "adhoc_overloading" uncheck);
    9.10 +  (Syntax_Phases.context_term_check 0 "adhoc_overloading" check
    9.11 +   #> Syntax_Phases.context_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
    9.12 +   #> Syntax_Phases.context_term_uncheck 0 "adhoc_overloading" uncheck);
    9.13  
    9.14  end;
    10.1 --- a/src/Tools/subtyping.ML	Wed Nov 09 19:01:50 2011 +0100
    10.2 +++ b/src/Tools/subtyping.ML	Wed Nov 09 20:47:11 2011 +0100
    10.3 @@ -806,7 +806,7 @@
    10.4  val coercion_enabled = Attrib.setup_config_bool @{binding coercion_enabled} (K false);
    10.5  
    10.6  val add_term_check =
    10.7 -  Syntax.add_term_check ~100 "coercions"
    10.8 +  Syntax_Phases.term_check ~100 "coercions"
    10.9      (fn ctxt => Config.get ctxt coercion_enabled ? coercion_infer_types ctxt);
   10.10  
   10.11