src/HOL/Tools/datatype_codegen.ML
changeset 22921 475ff421a6a3
parent 22778 a5b87573f427
child 23513 2ebb50c0db4f
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Thu May 10 10:21:50 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu May 10 10:22:17 2007 +0200
     1.3 @@ -285,12 +285,12 @@
     1.4     (c as Const (s, T), ts) =>
     1.5       (case DatatypePackage.datatype_of_case thy s of
     1.6          SOME {index, descr, ...} =>
     1.7 -          if is_some (get_assoc_code thy s T) then NONE else
     1.8 +          if is_some (get_assoc_code thy (s, T)) then NONE else
     1.9            SOME (pretty_case thy defs gr dep module brack
    1.10              (#3 (the (AList.lookup op = descr index))) c ts)
    1.11        | NONE => case (DatatypePackage.datatype_of_constr thy s, strip_type T) of
    1.12          (SOME {index, descr, ...}, (_, U as Type _)) =>
    1.13 -          if is_some (get_assoc_code thy s T) then NONE else
    1.14 +          if is_some (get_assoc_code thy (s, T)) then NONE else
    1.15            let val SOME args = AList.lookup op =
    1.16              (#3 (the (AList.lookup op = descr index))) s
    1.17            in
    1.18 @@ -305,7 +305,7 @@
    1.19        (case DatatypePackage.get_datatype thy s of
    1.20           NONE => NONE
    1.21         | SOME {descr, ...} =>
    1.22 -           if isSome (get_assoc_type thy s) then NONE else
    1.23 +           if is_some (get_assoc_type thy s) then NONE else
    1.24             let
    1.25               val (gr', ps) = foldl_map
    1.26                 (invoke_tycodegen thy defs dep module false) (gr, Ts);