src/HOL/Tools/datatype_package.ML
changeset 21187 16fb5afbf228
parent 21127 c8e862897d13
child 21243 afffe1f72143
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Sun Nov 05 21:44:41 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Sun Nov 05 21:44:42 2006 +0100
     1.3 @@ -402,8 +402,12 @@
     1.4        val thy = Context.theory_of context;
     1.5        fun case_error s name ts = raise TERM ("Error in case expression" ^
     1.6          getOpt (Option.map (curry op ^ " for datatype ") name, "") ^ ":\n" ^ s, ts);
     1.7 -      fun dest_case1 (Const ("_case1", _) $ t $ u) = (case strip_comb t of
     1.8 -            (Const (s, _), ts) => (((perhaps o try o unprefix) Syntax.constN o Sign.intern_const thy) s, ts)
     1.9 +      fun dest_case1 (Const ("_case1", _) $ t $ u) =
    1.10 +          (case strip_comb t of
    1.11 +            (Const (s, _), ts) =>
    1.12 +              (case try (unprefix Syntax.constN) s of
    1.13 +                SOME c => (c, ts)
    1.14 +              | NONE => (Sign.intern_const thy s, ts))
    1.15            | (Free (s, _), ts) => (Sign.intern_const thy s, ts) (*FIXME?*)
    1.16            | _ => case_error "Head is not a constructor" NONE [t, u], u)
    1.17          | dest_case1 t = raise TERM ("dest_case1", [t]);