src/HOL/Tools/Datatype/rep_datatype.ML
changeset 56245 84fc7dfa3cd4
parent 56239 17df7145a871
child 56254 a2dd9200854d
     1.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -434,7 +434,7 @@
     1.4    let
     1.5      fun prove_case_cong ((t, nchotomy), case_rewrites) =
     1.6        let
     1.7 -        val Const ("==>", _) $ tm $ _ = t;
     1.8 +        val Const (@{const_name Pure.imp}, _) $ tm $ _ = t;
     1.9          val Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma) = tm;
    1.10          val cert = cterm_of thy;
    1.11          val nchotomy' = nchotomy RS spec;