# HG changeset patch
# User traytel
# Date 1362387474 -3600
# Node ID 62c033d7f3d8ad84c16d6cc2b1616070e2d88013
# Parent  a75040aaf369b60e44a601740bf62ae1629abf00
tuned (extend datatype to inline option)

diff -r a75040aaf369 -r 62c033d7f3d8 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Sun Mar 03 18:50:46 2013 +0100
+++ b/src/Tools/subtyping.ML	Mon Mar 04 09:57:54 2013 +0100
@@ -20,7 +20,7 @@
 (** coercions data **)
 
 datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT | INVARIANT_TO of typ;
-datatype coerce_arg = PERMIT | FORBID
+datatype coerce_arg = PERMIT | FORBID | LEAVE
 
 datatype data = Data of
   {coes: (term * ((typ list * typ list) * term list)) Symreltab.table,  (*coercions table*)
@@ -29,7 +29,7 @@
    (*coercions graph restricted to base types - for efficiency reasons strored in the context*)
    coes_graph: int Graph.T,
    tmaps: (term * variance list) Symtab.table,  (*map functions*)
-   coerce_args: coerce_arg option list Symtab.table  (*special constants with non-coercible arguments*)};
+   coerce_args: coerce_arg list Symtab.table  (*special constants with non-coercible arguments*)};
 
 fun make_data (coes, full_graph, coes_graph, tmaps, coerce_args) =
   Data {coes = coes, full_graph = full_graph, coes_graph = coes_graph,
@@ -297,8 +297,7 @@
   let
     val mk_coerce_args = the_default [] o Symtab.lookup (coerce_args_of ctxt);
     fun update _ [] = old
-      | update 0 (coerce :: _) =
-        (case coerce of NONE => old | SOME PERMIT => true | SOME FORBID => false)
+      | update 0 (coerce :: _) = (case coerce of LEAVE => old | PERMIT => true | FORBID => false)
       | update n (_ :: cs) = update (n - 1) cs;
     val (f, n) = Term.strip_comb (Type.strip_constraints t) ||> length;
   in
@@ -1054,9 +1053,7 @@
 (* theory setup *)
 
 val parse_coerce_args =
-  Args.$$$ "+" >> K (SOME PERMIT) ||
-  Args.$$$ "-" >> K (SOME FORBID) ||
-  Args.$$$ "0" >> K NONE
+  Args.$$$ "+" >> K PERMIT || Args.$$$ "-" >> K FORBID || Args.$$$ "0" >> K LEAVE
 
 val setup =
   Context.theory_map add_term_check #>